val error : ?loc:Ast.Loc.t -> string -> 'aA regular error (fatal)
val anomaly : ?loc:Ast.Loc.t -> string -> 'aAn invariant is broken, i.e. a bug
val type_error : ?loc:Ast.Loc.t -> string -> 'aA type error (in principle ruled out by elpi-checker.elpi)
val warn : ?loc:Ast.Loc.t -> string -> unitA non fatal warning
link between OCaml and LP lists. Note that 1,2|X is not a valid * OCaml list!
val get_assignment : FlexibleData.Elpi.t -> Data.term optionThe body of an assignment, if any (LOW LEVEL). * Use look and forget about this API since the term you get * needs to be moved and/or reduced, and you have no API for this.
val clause_of_term :
?name:string ->
?graft:([ `After | `Before | `Replace | `Remove ] * string) ->
depth:int ->
Ast.Loc.t ->
Data.term ->
Ast.programHackish, in particular the output should be a compiled program
val term_to_raw_term :
State.t ->
Compile.program ->
?ctx:RawData.constant Ast.Scope.Map.t ->
depth:int ->
Ast.Term.t ->
Data.termHackish
Lifting/restriction/beta (LOW LEVEL, don't use)
val map_acc :
(State.t -> 't -> State.t * 'a * Conversion.extra_goals) ->
State.t ->
't list ->
State.t * 'a list * Conversion.extra_goalsreadback/embed on lists
module type Show = sig ... endmodule type Show1 = sig ... endmodule Map : sig ... endmodule Set : sig ... end