type quotation = depth:int -> State.t -> Ast.Loc.t -> string -> State.t * Data.term
val set_default_quotation : quotation -> unit

The default quotation {{code}}

val register_named_quotation : name:string -> quotation -> unit

Named quotation {{name:code}}

val lp : quotation

The anti-quotation to lambda Prolog

val quote_syntax_runtime : State.t -> 'a Compile.query -> State.t * Data.term list * Data.term

See elpi-quoted_syntax.elpi (EXPERIMENTAL, used by elpi-checker)

val quote_syntax_compiletime : State.t -> 'a Compile.query -> State.t * Data.term list * Data.term
val term_at : depth:int -> State.t -> Ast.query -> State.t * Data.term

To implement the string_to_term built-in (AVOID, makes little sense * if depth is non zero, since bound variables have no name!)

Like quotations but for identifiers that begin and end with * "`" or "'", e.g. `this` and 'that'. Useful if the object language * needs something that looks like a string but with a custom compilation * (e.g. CD.string like but with a case insensitive comparison)

val declare_backtick : name:string -> (State.t -> string -> State.t * Data.term) -> unit
val declare_singlequote : name:string -> (State.t -> string -> State.t * Data.term) -> unit