kind abbreviation type. kind argument type. kind argument_mode type. kind arity type. kind attribute type. kind attribute-value type. kind bool type. kind class type. kind clause type. kind cmp type. kind coercion type. kind coercion-status type. kind constant type. kind constructor type. kind context-decl type. kind conversion_strategy type. kind coq.gref.map type -> type. kind coq.gref.set type. kind coq.inline type. kind coq.option type. kind coq.pp type. kind coq.pp.box type. kind coq.redflag type. kind coq.redflags type. kind coq.univ.map type -> type. kind coq.univ.set type. kind coq.univ.variable.map type -> type. kind coq.univ.variable.set type. kind cs-instance type. kind cs-pattern type. kind diagnostic type. kind evarkey type. kind field-attribute type. kind float type. kind float64 type. kind goal type. kind grafting type. kind gref type. kind group type. kind hint-mode type. kind implicit_kind type. kind in_stream type. kind indc-decl type. kind indt-decl type. kind inductive type. kind int type. kind list type -> type. kind loc type. kind located type. kind ltac1-tactic type. kind modpath type. kind modtypath type. kind module-item type. kind name type. kind option type -> type. kind out_stream type. kind pair type -> type -> type. kind primitive-value type. kind projection type. kind pstring type. kind record-decl type. kind safe type. kind scope type. kind sealed-goal type. kind simplification_strategy type. kind sort type. kind std.int.map type -> type. kind std.int.set type. kind std.loc.map type -> type. kind std.loc.set type. kind std.map type -> type -> type. kind std.map.private.map type -> type -> type. kind std.set type -> type. kind std.set.private.set type -> type. kind std.string.map type -> type. kind std.string.set type. kind string type. kind synterp-action type. kind tc-instance type. kind term type. kind triple type -> type -> type -> type. kind ty type. kind uint63 type. kind univ type. kind univ-constraint type. kind univ-instance type. kind univ-variance type. kind univ.variable type. kind unix.process type. kind upoly-decl type. kind upoly-decl-cumul type. type ! prop. type (*) int -> int -> int. type (*) float -> float -> float. type (+) int -> int -> int. type (+) float -> float -> float. type (,) prop ..-> prop. type (-) A -> A -> A. type (/) float -> float -> float. type (:-) prop -> prop -> prop. type (:-) prop -> list prop -> prop. type (::) X -> list X -> list X. type (;) prop -> prop -> prop. type (<) A -> A -> prop. type (=) A -> A -> prop. type (=<) A -> A -> prop. type (==) A -> A -> prop. type (=>) prop -> prop -> prop. type (=>) list prop -> prop -> prop. type (>) A -> A -> prop. type (>=) A -> A -> prop. type [] list X. type (^) string -> string -> string. type abs int -> int. type abs float -> float. type after id -> grafting. type app term -> term -> term. type app list term -> term. type apply-module-functor id -> synterp-action. type apply-module-type-functor id -> synterp-action. type arctan float -> float. type arity term -> arity. type arr ty -> ty -> ty. type as A -> A -> A. type attribute string -> attribute-value -> attribute. type attributes list attribute -> prop. type auto univ.variable -> univ-variance. type bar term. type before id -> grafting. type begin-module id -> synterp-action. type begin-module-type id -> synterp-action. type begin-section id -> synterp-action. type calc A -> A -> prop. type canonical bool -> field-attribute. type ceil float -> int. type chr int -> string. type clause id -> grafting -> prop -> clause. type close_in in_stream -> prop. type close_out out_stream -> prop. type closed_term any -> prop. type cmp_term any -> any -> cmp -> prop. type coercion coercion-status -> field-attribute. type coercion gref -> int -> gref -> class -> coercion. type const constant -> gref. type const-decl id -> option term -> arity -> argument. type constant any -> any ..-> prop. type constructor id -> arity -> indc-decl. type context-end context-decl. type context-item id -> implicit_kind -> term -> option term -> (term -> context-decl) -> context-decl. type coq.CS.canonical-projections inductive -> list (option constant) -> prop. type coq.CS.db list cs-instance -> prop. type coq.CS.db-for gref -> cs-pattern -> list cs-instance -> prop. type coq.CS.declare-instance gref -> prop. type coq.TC.class? gref -> prop. type coq.TC.db list tc-instance -> prop. type coq.TC.db-for gref -> list tc-instance -> prop. type coq.TC.db-tc list gref -> prop. type coq.TC.declare-class gref -> prop. type coq.TC.declare-instance gref -> int -> prop. type coq.TC.get-inst-prio gref -> gref -> int -> prop. type coq.arguments.implicit gref -> list (list implicit_kind) -> prop. type coq.arguments.name gref -> list (option id) -> prop. type coq.arguments.scope gref -> list (list id) -> prop. type coq.arguments.set-default-implicit gref -> prop. type coq.arguments.set-implicit gref -> list (list implicit_kind) -> prop. type coq.arguments.set-name gref -> list (option id) -> prop. type coq.arguments.set-scope gref -> list (list id) -> prop. type coq.arguments.set-simplification gref -> simplification_strategy -> prop. type coq.arguments.simplification gref -> option simplification_strategy -> prop. type coq.begin-synterp-group id -> group -> prop. type coq.coercion.db list coercion -> prop. type coq.coercion.db-for class -> class -> list (pair gref int) -> prop. type coq.coercion.declare coercion -> prop. type coq.debug any ..-> prop. type coq.elaborate-skeleton term -> term -> term -> diagnostic -> prop. type coq.elaborate-ty-skeleton term -> sort -> term -> diagnostic -> prop. type coq.elpi.accumulate scope -> id -> clause -> prop. type coq.elpi.accumulate-clauses scope -> id -> list clause -> prop. type coq.elpi.add-predicate string -> string -> string -> list (pair argument_mode string) -> prop. type coq.elpi.predicate string -> list any -> prop -> prop. type coq.elpi.toposort list (pair A (list A)) -> list A -> prop. type coq.end-synterp-group group -> prop. type coq.env.add-axiom id -> term -> constant -> prop. type coq.env.add-const id -> term -> term -> opaque? -> constant -> prop. type coq.env.add-indt indt-decl -> inductive -> prop. type coq.env.add-section-variable id -> term -> constant -> prop. type coq.env.apply-module-functor id -> option modtypath -> modpath -> list modpath -> coq.inline -> modpath -> prop. type coq.env.apply-module-type-functor id -> modtypath -> list modpath -> coq.inline -> modtypath -> prop. type coq.env.begin-module id -> option modtypath -> prop. type coq.env.begin-module-functor id -> option modtypath -> list (pair id modtypath) -> prop. type coq.env.begin-module-type id -> prop. type coq.env.begin-module-type-functor id -> list (pair id modtypath) -> prop. type coq.env.begin-section id -> prop. type coq.env.const constant -> option term -> term -> prop. type coq.env.const-body constant -> option term -> prop. type coq.env.const-opaque? constant -> prop. type coq.env.const-primitive? constant -> prop. type coq.env.current-path list string -> prop. type coq.env.current-section-path list string -> prop. type coq.env.dependencies gref -> modpath -> coq.gref.set -> prop. type coq.env.end-module modpath -> prop. type coq.env.end-module-type modtypath -> prop. type coq.env.end-section prop. type coq.env.export-module modpath -> prop. type coq.env.fresh-global-id id -> id -> prop. type coq.env.global gref -> term -> prop. type coq.env.import-module modpath -> prop. type coq.env.include-module modpath -> coq.inline -> prop. type coq.env.include-module-type modtypath -> coq.inline -> prop. type coq.env.indc constructor -> int -> int -> int -> term -> prop. type coq.env.indc->indt constructor -> inductive -> int -> prop. type coq.env.indt inductive -> bool -> int -> int -> term -> list constructor -> list term -> prop. type coq.env.indt-decl inductive -> indt-decl -> prop. type coq.env.informative? inductive -> prop. type coq.env.module modpath -> list module-item -> prop. type coq.env.module-type modtypath -> list id -> prop. type coq.env.opaque? constant -> prop. type coq.env.primitive-projection? projection -> constant -> prop. type coq.env.primitive-projections inductive -> list (option (pair projection int)) -> prop. type coq.env.primitive? constant -> prop. type coq.env.projection? constant -> int -> prop. type coq.env.projections inductive -> list (option constant) -> prop. type coq.env.record? inductive -> bool -> prop. type coq.env.recursive? inductive -> prop. type coq.env.section list constant -> prop. type coq.env.term-dependencies term -> coq.gref.set -> prop. type coq.env.transitive-dependencies gref -> modpath -> coq.gref.set -> prop. type coq.env.typeof gref -> term -> prop. type coq.env.univpoly? gref -> int -> prop. type coq.error any ..-> prop. type coq.extra-dep id -> option id -> prop. type coq.float->float64 float -> float64 -> prop. type coq.float64->float float64 -> float -> prop. type coq.goal->pp goal -> coq.pp -> prop. type coq.gref->id gref -> id -> prop. type coq.gref->path gref -> list string -> prop. type coq.gref->string gref -> string -> prop. type coq.gref.map.add gref -> A -> coq.gref.map A -> coq.gref.map A -> prop. type coq.gref.map.bindings coq.gref.map A -> list (pair gref A) -> prop. type coq.gref.map.empty coq.gref.map A -> prop. type coq.gref.map.filter coq.gref.map A -> (gref -> A -> prop) -> coq.gref.map A -> prop. type coq.gref.map.find gref -> coq.gref.map A -> A -> prop. type coq.gref.map.fold coq.gref.map A -> C -> (gref -> A -> C -> C -> prop) -> C -> prop. type coq.gref.map.map coq.gref.map A -> (gref -> A -> B -> prop) -> coq.gref.map B -> prop. type coq.gref.map.mem gref -> coq.gref.map A -> prop. type coq.gref.map.remove gref -> coq.gref.map A -> coq.gref.map A -> prop. type coq.gref.set.add gref -> coq.gref.set -> coq.gref.set -> prop. type coq.gref.set.cardinal coq.gref.set -> int -> prop. type coq.gref.set.choose coq.gref.set -> gref -> prop. type coq.gref.set.diff coq.gref.set -> coq.gref.set -> coq.gref.set -> prop. type coq.gref.set.elements coq.gref.set -> list gref -> prop. type coq.gref.set.empty coq.gref.set -> prop. type coq.gref.set.equal coq.gref.set -> coq.gref.set -> prop. type coq.gref.set.filter coq.gref.set -> (gref -> prop) -> coq.gref.set -> prop. type coq.gref.set.fold coq.gref.set -> A -> (gref -> A -> A -> prop) -> A -> prop. type coq.gref.set.inter coq.gref.set -> coq.gref.set -> coq.gref.set -> prop. type coq.gref.set.map coq.gref.set -> (gref -> gref -> prop) -> coq.gref.set -> prop. type coq.gref.set.max coq.gref.set -> gref -> prop. type coq.gref.set.mem gref -> coq.gref.set -> prop. type coq.gref.set.min coq.gref.set -> gref -> prop. type coq.gref.set.partition coq.gref.set -> (gref -> prop) -> coq.gref.set -> coq.gref.set -> prop. type coq.gref.set.remove gref -> coq.gref.set -> coq.gref.set -> prop. type coq.gref.set.subset coq.gref.set -> coq.gref.set -> prop. type coq.gref.set.union coq.gref.set -> coq.gref.set -> coq.gref.set -> prop. type coq.hints.add-mode gref -> string -> list hint-mode -> prop. type coq.hints.add-resolve gref -> string -> int -> term -> prop. type coq.hints.modes gref -> string -> list (list hint-mode) -> prop. type coq.hints.opaque constant -> string -> bool -> prop. type coq.hints.set-opaque constant -> string -> bool -> prop. type coq.id->name id -> name -> prop. type coq.info any ..-> prop. type coq.inline.at int -> coq.inline. type coq.inline.default coq.inline. type coq.inline.no coq.inline. type coq.int->uint63 int -> uint63 -> prop. type coq.locate id -> gref -> prop. type coq.locate-abbreviation id -> abbreviation -> prop. type coq.locate-all id -> list located -> prop. type coq.locate-module id -> modpath -> prop. type coq.locate-module-type id -> modtypath -> prop. type coq.ltac.call-ltac1 any -> goal -> list sealed-goal -> prop. type coq.ltac.collect-goals term -> list sealed-goal -> list sealed-goal -> prop. type coq.ltac.fail int -> any ..-> prop. type coq.ltac.fresh-id id -> term -> id -> prop. type coq.ltac.id-free? id -> goal -> prop. type coq.modpath->library modpath -> modpath -> prop. type coq.modpath->path modpath -> list string -> prop. type coq.modtypath->library modtypath -> modpath -> prop. type coq.modtypath->path modtypath -> list string -> prop. type coq.name->id name -> id -> prop. type coq.name-suffix name -> any -> name -> prop. type coq.next-synterp-action synterp-action -> prop. type coq.notation.abbreviation abbreviation -> list term -> term -> prop. type coq.notation.abbreviation-body abbreviation -> int -> term -> prop. type coq.notation.add-abbreviation id -> int -> term -> bool -> abbreviation -> prop. type coq.notation.add-abbreviation-for-tactic string -> string -> list argument -> prop. type coq.notice any ..-> prop. type coq.option.add list string -> coq.option -> bool -> prop. type coq.option.available? list string -> bool -> prop. type coq.option.bool bool -> coq.option. type coq.option.get list string -> coq.option -> prop. type coq.option.int option int -> coq.option. type coq.option.set list string -> coq.option -> prop. type coq.option.string option string -> coq.option. type coq.pp->string coq.pp -> string -> prop. type coq.pp.box coq.pp.box -> list coq.pp -> coq.pp. type coq.pp.brk int -> int -> coq.pp. type coq.pp.comment list string -> coq.pp. type coq.pp.empty coq.pp. type coq.pp.glue list coq.pp -> coq.pp. type coq.pp.h coq.pp.box. type coq.pp.hov int -> coq.pp.box. type coq.pp.hv int -> coq.pp.box. type coq.pp.nl coq.pp. type coq.pp.spc coq.pp. type coq.pp.str string -> coq.pp. type coq.pp.tag string -> coq.pp -> coq.pp. type coq.pp.v int -> coq.pp.box. type coq.primitive.projection-unfolded projection -> projection -> prop. type coq.pstring->string pstring -> string -> prop. type coq.redflags.add coq.redflags -> list coq.redflag -> coq.redflags -> prop. type coq.redflags.all coq.redflags. type coq.redflags.allnolet coq.redflags. type coq.redflags.beta coq.redflag. type coq.redflags.beta coq.redflags. type coq.redflags.betadeltazeta coq.redflags. type coq.redflags.betaiota coq.redflags. type coq.redflags.betaiotazeta coq.redflags. type coq.redflags.betazeta coq.redflags. type coq.redflags.cofix coq.redflag. type coq.redflags.const constant -> coq.redflag. type coq.redflags.delta coq.redflag. type coq.redflags.delta coq.redflags. type coq.redflags.fix coq.redflag. type coq.redflags.match coq.redflag. type coq.redflags.nored coq.redflags. type coq.redflags.sub coq.redflags -> list coq.redflag -> coq.redflags -> prop. type coq.redflags.zeta coq.redflag. type coq.redflags.zeta coq.redflags. type coq.reduction.cbv.norm term -> term -> prop. type coq.reduction.cbv.whd_all term -> term -> prop. type coq.reduction.eta-contract term -> term -> prop. type coq.reduction.lazy.bi-norm term -> term -> prop. type coq.reduction.lazy.norm term -> term -> prop. type coq.reduction.lazy.whd term -> term -> prop. type coq.reduction.lazy.whd_all term -> term -> prop. type coq.reduction.native.available? prop. type coq.reduction.native.norm term -> term -> term -> prop. type coq.reduction.vm.norm term -> term -> term -> prop. type coq.reduction.vm.whd_all term -> term -> term -> prop. type coq.replay-synterp-action-group id -> prop. type coq.say any ..-> prop. type coq.sigma.print prop. type coq.sort.eq sort -> sort -> prop. type coq.sort.leq sort -> sort -> prop. type coq.sort.pts-triple sort -> sort -> sort -> prop. type coq.sort.sup sort -> sort -> prop. type coq.strategy.get constant -> conversion_strategy -> prop. type coq.strategy.set list constant -> conversion_strategy -> prop. type coq.string->name string -> name -> prop. type coq.string->pstring string -> pstring -> prop. type coq.term->pp term -> coq.pp -> prop. type coq.term->string term -> string -> prop. type coq.typecheck term -> term -> diagnostic -> prop. type coq.typecheck-ty term -> sort -> diagnostic -> prop. type coq.uint63->int uint63 -> int -> prop. type coq.unify-eq term -> term -> diagnostic -> prop. type coq.unify-leq term -> term -> diagnostic -> prop. type coq.univ id -> univ -> prop. type coq.univ-instance univ-instance -> list univ.variable -> prop. type coq.univ-instance.unify-eq gref -> univ-instance -> univ-instance -> diagnostic -> prop. type coq.univ-instance.unify-leq gref -> univ-instance -> univ-instance -> diagnostic -> prop. type coq.univ.constraints list univ-constraint -> prop. type coq.univ.global? univ -> prop. type coq.univ.map.add univ -> A -> coq.univ.map A -> coq.univ.map A -> prop. type coq.univ.map.bindings coq.univ.map A -> list (pair univ A) -> prop. type coq.univ.map.empty coq.univ.map A -> prop. type coq.univ.map.filter coq.univ.map A -> (univ -> A -> prop) -> coq.univ.map A -> prop. type coq.univ.map.find univ -> coq.univ.map A -> A -> prop. type coq.univ.map.fold coq.univ.map A -> C -> (univ -> A -> C -> C -> prop) -> C -> prop. type coq.univ.map.map coq.univ.map A -> (univ -> A -> B -> prop) -> coq.univ.map B -> prop. type coq.univ.map.mem univ -> coq.univ.map A -> prop. type coq.univ.map.remove univ -> coq.univ.map A -> coq.univ.map A -> prop. type coq.univ.new univ -> prop. type coq.univ.print prop. type coq.univ.set.add univ -> coq.univ.set -> coq.univ.set -> prop. type coq.univ.set.cardinal coq.univ.set -> int -> prop. type coq.univ.set.choose coq.univ.set -> univ -> prop. type coq.univ.set.diff coq.univ.set -> coq.univ.set -> coq.univ.set -> prop. type coq.univ.set.elements coq.univ.set -> list univ -> prop. type coq.univ.set.empty coq.univ.set -> prop. type coq.univ.set.equal coq.univ.set -> coq.univ.set -> prop. type coq.univ.set.filter coq.univ.set -> (univ -> prop) -> coq.univ.set -> prop. type coq.univ.set.fold coq.univ.set -> A -> (univ -> A -> A -> prop) -> A -> prop. type coq.univ.set.inter coq.univ.set -> coq.univ.set -> coq.univ.set -> prop. type coq.univ.set.map coq.univ.set -> (univ -> univ -> prop) -> coq.univ.set -> prop. type coq.univ.set.max coq.univ.set -> univ -> prop. type coq.univ.set.mem univ -> coq.univ.set -> prop. type coq.univ.set.min coq.univ.set -> univ -> prop. type coq.univ.set.partition coq.univ.set -> (univ -> prop) -> coq.univ.set -> coq.univ.set -> prop. type coq.univ.set.remove univ -> coq.univ.set -> coq.univ.set -> prop. type coq.univ.set.subset coq.univ.set -> coq.univ.set -> prop. type coq.univ.set.union coq.univ.set -> coq.univ.set -> coq.univ.set -> prop. type coq.univ.variable univ -> univ.variable -> prop. type coq.univ.variable.constraints univ.variable -> list univ-constraint -> prop. type coq.univ.variable.map.add univ.variable -> A -> coq.univ.variable.map A -> coq.univ.variable.map A -> prop. type coq.univ.variable.map.bindings coq.univ.variable.map A -> list (pair univ.variable A) -> prop. type coq.univ.variable.map.empty coq.univ.variable.map A -> prop. type coq.univ.variable.map.filter coq.univ.variable.map A -> (univ.variable -> A -> prop) -> coq.univ.variable.map A -> prop. type coq.univ.variable.map.find univ.variable -> coq.univ.variable.map A -> A -> prop. type coq.univ.variable.map.fold coq.univ.variable.map A -> C -> (univ.variable -> A -> C -> C -> prop) -> C -> prop. type coq.univ.variable.map.map coq.univ.variable.map A -> (univ.variable -> A -> B -> prop) -> coq.univ.variable.map B -> prop. type coq.univ.variable.map.mem univ.variable -> coq.univ.variable.map A -> prop. type coq.univ.variable.map.remove univ.variable -> coq.univ.variable.map A -> coq.univ.variable.map A -> prop. type coq.univ.variable.of-term term -> coq.univ.variable.set -> prop. type coq.univ.variable.set.add univ.variable -> coq.univ.variable.set -> coq.univ.variable.set -> prop. type coq.univ.variable.set.cardinal coq.univ.variable.set -> int -> prop. type coq.univ.variable.set.choose coq.univ.variable.set -> univ.variable -> prop. type coq.univ.variable.set.diff coq.univ.variable.set -> coq.univ.variable.set -> coq.univ.variable.set -> prop. type coq.univ.variable.set.elements coq.univ.variable.set -> list univ.variable -> prop. type coq.univ.variable.set.empty coq.univ.variable.set -> prop. type coq.univ.variable.set.equal coq.univ.variable.set -> coq.univ.variable.set -> prop. type coq.univ.variable.set.filter coq.univ.variable.set -> (univ.variable -> prop) -> coq.univ.variable.set -> prop. type coq.univ.variable.set.fold coq.univ.variable.set -> A -> (univ.variable -> A -> A -> prop) -> A -> prop. type coq.univ.variable.set.inter coq.univ.variable.set -> coq.univ.variable.set -> coq.univ.variable.set -> prop. type coq.univ.variable.set.map coq.univ.variable.set -> (univ.variable -> univ.variable -> prop) -> coq.univ.variable.set -> prop. type coq.univ.variable.set.max coq.univ.variable.set -> univ.variable -> prop. type coq.univ.variable.set.mem univ.variable -> coq.univ.variable.set -> prop. type coq.univ.variable.set.min coq.univ.variable.set -> univ.variable -> prop. type coq.univ.variable.set.partition coq.univ.variable.set -> (univ.variable -> prop) -> coq.univ.variable.set -> coq.univ.variable.set -> prop. type coq.univ.variable.set.remove univ.variable -> coq.univ.variable.set -> coq.univ.variable.set -> prop. type coq.univ.variable.set.subset coq.univ.variable.set -> coq.univ.variable.set -> prop. type coq.univ.variable.set.union coq.univ.variable.set -> coq.univ.variable.set -> coq.univ.variable.set -> prop. type coq.version string -> int -> int -> int -> prop. type coq.warn any ..-> prop. type coq.warning string -> string -> any ..-> prop. type cos float -> float. type counter string -> int -> prop. type covariant univ.variable -> univ-variance. type cs-default cs-pattern. type cs-gref gref -> cs-pattern. type cs-instance gref -> cs-pattern -> gref -> cs-instance. type cs-prod cs-pattern. type cs-sort sort -> cs-pattern. type ctx-decl context-decl -> argument. type current scope. type decl term -> name -> term -> prop. type declare-evar list prop -> term -> term -> term -> prop. type declare_constraint any -> any -> any ..-> prop. type def term -> name -> term -> term -> prop. type distinct_names list any -> prop. type (div) int -> int -> int. type dprint any ..-> prop. type end-module modpath -> synterp-action. type end-module-type modtypath -> synterp-action. type end-record record-decl. type end-section synterp-action. type eof in_stream -> prop. type eq cmp. type eq univ.variable -> univ.variable -> univ-constraint. type error string -> diagnostic. type evar term -> term -> term -> prop. type execution-site scope. type expand conversion_strategy. type explicit implicit_kind. type export-module modpath -> synterp-action. type fail prop. type false prop. type ff bool. type field field-attributes -> id -> term -> (term -> record-decl) -> record-decl. type findall_solutions prop -> list prop -> prop. type fix name -> int -> term -> (term -> term) -> term. type float64 float64 -> primitive-value. type floor float -> int. type flush out_stream -> prop. type foo term. type fst pair A B -> A -> prop. type fun (term -> term) -> term. type fun name -> term -> (term -> term) -> term. type funclass class. type gc.compact prop. type gc.full prop. type gc.get int -> int -> int -> int -> int -> int -> int -> int -> prop. type gc.major prop. type gc.minor prop. type gc.quick-stat float -> float -> float -> int -> int -> int -> int -> int -> int -> int -> prop. type gc.set int -> int -> int -> int -> int -> int -> int -> int -> prop. type gc.stat float -> float -> float -> int -> int -> int -> int -> int -> int -> int -> int -> int -> int -> int -> int -> int -> prop. type ge_ A -> A -> prop. type get-option string -> A -> prop. type getenv string -> option string -> prop. type gettimeofday float -> prop. type global gref -> term. type goal goal-ctx -> term -> term -> term -> list argument -> goal. type gref gref -> module-item. type grefclass gref -> class. type ground_term any -> prop. type gt cmp. type gt_ A -> A -> prop. type halt any ..-> prop. type (i+) int -> int -> int. type (i-) int -> int -> int. type (i<) int -> int -> prop. type (i=<) int -> int -> prop. type (i>) int -> int -> prop. type (i>=) int -> int -> prop. type iabs int -> int. type if prop -> prop -> prop -> prop. type if2 prop -> prop -> prop -> prop -> prop -> prop. type implicit implicit_kind. type import-module modpath -> synterp-action. type in argument_mode. type include-module modpath -> synterp-action. type include-module-type modtypath -> synterp-action. type indc constructor -> gref. type indt inductive -> gref. type indt-decl indt-decl -> argument. type inductive id -> bool -> arity -> (term -> list indc-decl) -> indt-decl. type input in_stream -> int -> string -> prop. type input_line in_stream -> string -> prop. type int int -> argument. type int_to_real int -> float. type int_to_string int -> string. type invariant univ.variable -> univ-variance. type irrelevant univ.variable -> univ-variance. type (is) A -> A -> prop. type (is_cdata) any -> string -> prop. type (i~) int -> int. type le univ.variable -> univ.variable -> univ-constraint. type le_ A -> A -> prop. type leaf-loc loc -> attribute-value. type leaf-str string -> attribute-value. type let name -> term -> term -> (term -> term) -> term. type level int -> conversion_strategy. type library scope. type ln float -> float. type loc-abbreviation abbreviation -> located. type loc-gref gref -> located. type loc-modpath modpath -> located. type loc-modtypath modtypath -> located. type loc.fields loc -> string -> int -> int -> int -> int -> prop. type lookahead in_stream -> string -> prop. type lt cmp. type lt univ.variable -> univ.variable -> univ-constraint. type lt_ A -> A -> prop. type main list argument -> prop. type main-interp list argument -> any -> prop. type main-synterp list argument -> any -> prop. type match term -> term -> list term -> term. type max int -> int -> int. type max float -> float -> float. type maximal implicit_kind. type min int -> int -> int. type min float -> float -> float. type (mod) int -> int -> int. type (mode-ground) hint-mode. type (mode-input) hint-mode. type (mode-output) hint-mode. type (module-functor) modpath -> list modtypath -> module-item. type (module-type) modtypath -> module-item. type (module-type-functor) modtypath -> list modtypath -> module-item. type msolve list sealed-goal -> list sealed-goal -> prop. type nabla (term -> sealed-goal) -> sealed-goal. type name any -> any ..-> prop. type names list any -> prop. type never simplification_strategy. type new_int int -> prop. type new_safe safe -> prop. type node list attribute -> attribute-value. type none option A. type not prop -> prop. type occurs any -> any -> prop. type of term -> ty -> prop. type off coercion-status. type ok diagnostic. type opaque conversion_strategy. type open-trm int -> term -> argument. type open_append string -> out_stream -> prop. type open_in string -> in_stream -> prop. type open_out string -> out_stream -> prop. type open_safe safe -> list A -> prop. type open_string string -> in_stream -> prop. type out argument_mode. type output out_stream -> string -> prop. type parameter id -> implicit_kind -> term -> (term -> arity) -> arity. type parameter id -> implicit_kind -> term -> (term -> indt-decl) -> indt-decl. type pglobal gref -> univ-instance -> term. type pi (A -> prop) -> prop. type pr A -> B -> pair A B. type primitive primitive-value -> term. type primitive? A -> string -> prop. type print any ..-> prop. type print_constraints prop. type printterm out_stream -> A -> prop. type prod name -> term -> (term -> term) -> term. type proj projection -> int -> primitive-value. type prop sort. type prune any -> list any -> prop. type pstring pstring -> primitive-value. type (r+) float -> float -> float. type (r-) float -> float -> float. type (r<) float -> float -> prop. type (r=<) float -> float -> prop. type (r>) float -> float -> prop. type (r>=) float -> float -> prop. type rabs float -> float. type random.init int -> prop. type random.int int -> int -> prop. type random.self_init prop. type real_to_string float -> string. type record id -> term -> id -> record-decl -> indt-decl. type regular coercion-status. type remove id -> grafting. type replace id -> grafting. type reversible coercion-status. type rex.match string -> string -> prop. type rex.replace string -> string -> string -> string -> prop. type rex.split string -> string -> list string -> prop. type rex_match string -> string -> prop. type rex_replace string -> string -> string -> string -> prop. type rex_split string -> string -> list string -> prop. type rhc string -> int. type rm-evar term -> term -> prop. type (r~) float -> float. type (s<) string -> string -> prop. type (s=<) string -> string -> prop. type (s>) string -> string -> prop. type (s>=) string -> string -> prop. type same_term A -> A -> prop. type same_var A -> A -> prop. type seal goal -> sealed-goal. type sigma (A -> prop) -> prop. type sin float -> float. type size string -> int. type snd pair A B -> B -> prop. type solve goal -> list sealed-goal -> prop. type some A -> option A. type sort sort -> term. type sortclass class. type sprop sort. type sqrt float -> float. type stash_in_safe safe -> A -> prop. type std.any->string A -> string -> prop. type std.append list A -> list A -> list A -> prop. type std.appendR list A -> list A -> list A -> prop. type std.assert! prop -> string -> prop. type std.assert-ok! (diagnostic -> prop) -> string -> prop. type std.debug-print string -> A -> prop. type std.do! list prop -> prop. type std.do-ok! diagnostic -> list (diagnostic -> prop) -> prop. type std.drop int -> list A -> list A -> prop. type std.drop-last int -> list A -> list A -> prop. type std.exists list A -> (A -> prop) -> prop. type std.exists2 list A -> list B -> (A -> B -> prop) -> prop. type std.fatal-error string -> prop. type std.fatal-error-w-data string -> A -> prop. type std.filter list A -> (A -> prop) -> list A -> prop. type std.findall prop -> list prop -> prop. type std.flatten list (list A) -> list A -> prop. type std.flip (A -> B -> prop) -> B -> A -> prop. type std.fold list B -> A -> (B -> A -> A -> prop) -> A -> prop. type std.fold-map list A -> B -> (A -> B -> C -> B -> prop) -> list C -> B -> prop. type std.fold-right list B -> A -> (B -> A -> A -> prop) -> A -> prop. type std.fold2 list C -> list B -> A -> (C -> B -> A -> A -> prop) -> A -> prop. type std.forall list A -> (A -> prop) -> prop. type std.forall-ok list A -> (A -> diagnostic -> prop) -> diagnostic -> prop. type std.forall2 list A -> list B -> (A -> B -> prop) -> prop. type std.ignore-failure! prop -> prop. type std.int.map.add int -> A -> std.int.map A -> std.int.map A -> prop. type std.int.map.bindings std.int.map A -> list (pair int A) -> prop. type std.int.map.empty std.int.map A -> prop. type std.int.map.filter std.int.map A -> (int -> A -> prop) -> std.int.map A -> prop. type std.int.map.find int -> std.int.map A -> A -> prop. type std.int.map.fold std.int.map A -> C -> (int -> A -> C -> C -> prop) -> C -> prop. type std.int.map.map std.int.map A -> (int -> A -> B -> prop) -> std.int.map B -> prop. type std.int.map.mem int -> std.int.map A -> prop. type std.int.map.remove int -> std.int.map A -> std.int.map A -> prop. type std.int.set.add int -> std.int.set -> std.int.set -> prop. type std.int.set.cardinal std.int.set -> int -> prop. type std.int.set.choose std.int.set -> int -> prop. type std.int.set.diff std.int.set -> std.int.set -> std.int.set -> prop. type std.int.set.elements std.int.set -> list int -> prop. type std.int.set.empty std.int.set -> prop. type std.int.set.equal std.int.set -> std.int.set -> prop. type std.int.set.filter std.int.set -> (int -> prop) -> std.int.set -> prop. type std.int.set.fold std.int.set -> A -> (int -> A -> A -> prop) -> A -> prop. type std.int.set.inter std.int.set -> std.int.set -> std.int.set -> prop. type std.int.set.map std.int.set -> (int -> int -> prop) -> std.int.set -> prop. type std.int.set.max std.int.set -> int -> prop. type std.int.set.mem int -> std.int.set -> prop. type std.int.set.min std.int.set -> int -> prop. type std.int.set.partition std.int.set -> (int -> prop) -> std.int.set -> std.int.set -> prop. type std.int.set.remove int -> std.int.set -> std.int.set -> prop. type std.int.set.subset std.int.set -> std.int.set -> prop. type std.int.set.union std.int.set -> std.int.set -> std.int.set -> prop. type std.intersperse A -> list A -> list A -> prop. type std.iota int -> list int -> prop. type std.last list A -> A -> prop. type std.length list A -> int -> prop. type std.lift-ok prop -> string -> diagnostic -> prop. type std.list.init int -> (int -> A -> prop) -> list A -> prop. type std.list.init.aux int -> int -> (int -> A -> prop) -> list A -> prop. type std.list.make int -> A -> list A -> prop. type std.loc.map.add loc -> A -> std.loc.map A -> std.loc.map A -> prop. type std.loc.map.bindings std.loc.map A -> list (pair loc A) -> prop. type std.loc.map.empty std.loc.map A -> prop. type std.loc.map.filter std.loc.map A -> (loc -> A -> prop) -> std.loc.map A -> prop. type std.loc.map.find loc -> std.loc.map A -> A -> prop. type std.loc.map.fold std.loc.map A -> C -> (loc -> A -> C -> C -> prop) -> C -> prop. type std.loc.map.map std.loc.map A -> (loc -> A -> B -> prop) -> std.loc.map B -> prop. type std.loc.map.mem loc -> std.loc.map A -> prop. type std.loc.map.remove loc -> std.loc.map A -> std.loc.map A -> prop. type std.loc.set.add loc -> std.loc.set -> std.loc.set -> prop. type std.loc.set.cardinal std.loc.set -> int -> prop. type std.loc.set.choose std.loc.set -> loc -> prop. type std.loc.set.diff std.loc.set -> std.loc.set -> std.loc.set -> prop. type std.loc.set.elements std.loc.set -> list loc -> prop. type std.loc.set.empty std.loc.set -> prop. type std.loc.set.equal std.loc.set -> std.loc.set -> prop. type std.loc.set.filter std.loc.set -> (loc -> prop) -> std.loc.set -> prop. type std.loc.set.fold std.loc.set -> A -> (loc -> A -> A -> prop) -> A -> prop. type std.loc.set.inter std.loc.set -> std.loc.set -> std.loc.set -> prop. type std.loc.set.map std.loc.set -> (loc -> loc -> prop) -> std.loc.set -> prop. type std.loc.set.max std.loc.set -> loc -> prop. type std.loc.set.mem loc -> std.loc.set -> prop. type std.loc.set.min std.loc.set -> loc -> prop. type std.loc.set.partition std.loc.set -> (loc -> prop) -> std.loc.set -> std.loc.set -> prop. type std.loc.set.remove loc -> std.loc.set -> std.loc.set -> prop. type std.loc.set.subset std.loc.set -> std.loc.set -> prop. type std.loc.set.union std.loc.set -> std.loc.set -> std.loc.set -> prop. type std.lookup list (pair A B) -> A -> B -> prop. type std.lookup! list (pair A B) -> A -> B -> prop. type std.map std.map.private.map K V -> (K -> K -> cmp -> prop) -> std.map K V. type std.map list A -> (A -> B -> prop) -> list B -> prop. type std.map-filter list A -> (A -> B -> prop) -> list B -> prop. type std.map-i list A -> (int -> A -> B -> prop) -> list B -> prop. type std.map-i.aux list A -> int -> (int -> A -> B -> prop) -> list B -> prop. type std.map-ok list A -> (A -> B -> diagnostic -> prop) -> list B -> diagnostic -> prop. type std.map.add K -> V -> std.map K V -> std.map K V -> prop. type std.map.bindings std.map K V -> list (pair K V) -> prop. type std.map.find K -> std.map K V -> V -> prop. type std.map.make (K -> K -> cmp -> prop) -> std.map K V -> prop. type std.map.private.add std.map.private.map K V -> (K -> K -> cmp -> prop) -> K -> V -> std.map.private.map K V -> prop. type std.map.private.add.aux cmp -> std.map.private.map K V -> (K -> K -> cmp -> prop) -> K -> V -> std.map.private.map K V -> prop. type std.map.private.bal std.map.private.map K V -> K -> V -> std.map.private.map K V -> std.map.private.map K V -> prop. type std.map.private.bal.aux int -> int -> int -> int -> std.map.private.map K V -> K -> V -> std.map.private.map K V -> std.map.private.map K V -> prop. type std.map.private.bindings std.map.private.map K V -> list (pair K V) -> list (pair K V) -> prop. type std.map.private.create std.map.private.map K V -> K -> V -> std.map.private.map K V -> std.map.private.map K V -> prop. type std.map.private.empty std.map.private.map K V. type std.map.private.find std.map.private.map K V -> (K -> K -> cmp -> prop) -> K -> V -> prop. type std.map.private.find.aux cmp -> (K -> K -> cmp -> prop) -> std.map.private.map K V -> std.map.private.map K V -> V -> K -> V -> prop. type std.map.private.height std.map.private.map K V -> int -> prop. type std.map.private.merge std.map.private.map K V -> std.map.private.map K V -> std.map.private.map K V -> prop. type std.map.private.min-binding std.map.private.map K V -> K -> V -> prop. type std.map.private.node std.map.private.map K V -> K -> V -> std.map.private.map K V -> int -> std.map.private.map K V. type std.map.private.remove std.map.private.map K V -> (K -> K -> cmp -> prop) -> K -> std.map.private.map K V -> prop. type std.map.private.remove-min-binding std.map.private.map K V -> std.map.private.map K V -> prop. type std.map.private.remove.aux cmp -> (K -> K -> cmp -> prop) -> std.map.private.map K V -> std.map.private.map K V -> K -> V -> K -> std.map.private.map K V -> prop. type std.map.remove K -> std.map K V -> std.map K V -> prop. type std.map2 list A -> list B -> (A -> B -> C -> prop) -> list C -> prop. type std.map2-filter list A -> list B -> (A -> B -> C -> prop) -> list C -> prop. type std.max A -> A -> A -> prop. type std.mem list A -> A -> prop. type std.mem! list A -> A -> prop. type std.nth int -> list A -> A -> prop. type std.null list A -> prop. type std.omap option A -> (A -> B -> prop) -> option B -> prop. type std.once prop -> prop. type std.rev list A -> list A -> prop. type std.rev.aux list A -> list A -> list A -> prop. type std.set std.set.private.set E -> (E -> E -> cmp -> prop) -> std.set E. type std.set.add E -> std.set E -> std.set E -> prop. type std.set.cardinal std.set E -> int -> prop. type std.set.elements std.set E -> list E -> prop. type std.set.make (E -> E -> cmp -> prop) -> std.set E -> prop. type std.set.mem E -> std.set E -> prop. type std.set.private.add std.set.private.set E -> (E -> E -> cmp -> prop) -> E -> std.set.private.set E -> prop. type std.set.private.add.aux cmp -> (E -> E -> cmp -> prop) -> std.set.private.set E -> std.set.private.set E -> E -> E -> int -> std.set.private.set E -> prop. type std.set.private.bal std.set.private.set E -> E -> std.set.private.set E -> std.set.private.set E -> prop. type std.set.private.bal.aux int -> int -> int -> int -> std.set.private.set E -> E -> std.set.private.set E -> std.set.private.set E -> prop. type std.set.private.cardinal std.set.private.set E -> int -> prop. type std.set.private.create std.set.private.set E -> E -> std.set.private.set E -> std.set.private.set E -> prop. type std.set.private.elements std.set.private.set E -> list E -> list E -> prop. type std.set.private.empty std.set.private.set E. type std.set.private.height std.set.private.set E -> int -> prop. type std.set.private.mem std.set.private.set E -> (E -> E -> cmp -> prop) -> E -> prop. type std.set.private.mem.aux cmp -> (E -> E -> cmp -> prop) -> std.set.private.set E -> std.set.private.set E -> E -> prop. type std.set.private.merge std.set.private.set E -> std.set.private.set E -> std.set.private.set E -> prop. type std.set.private.min-binding std.set.private.set E -> E -> prop. type std.set.private.node std.set.private.set E -> E -> std.set.private.set E -> int -> std.set.private.set E. type std.set.private.remove std.set.private.set E -> (E -> E -> cmp -> prop) -> E -> std.set.private.set E -> prop. type std.set.private.remove-min-binding std.set.private.set E -> std.set.private.set E -> prop. type std.set.private.remove.aux cmp -> (E -> E -> cmp -> prop) -> std.set.private.set E -> std.set.private.set E -> E -> E -> std.set.private.set E -> prop. type std.set.remove E -> std.set E -> std.set E -> prop. type std.split-at int -> list A -> list A -> list A -> prop. type std.spy prop -> prop. type std.spy! prop -> prop. type std.spy-do! list prop -> prop. type std.string.concat string -> list string -> string -> prop. type std.string.map.add string -> A -> std.string.map A -> std.string.map A -> prop. type std.string.map.bindings std.string.map A -> list (pair string A) -> prop. type std.string.map.empty std.string.map A -> prop. type std.string.map.filter std.string.map A -> (string -> A -> prop) -> std.string.map A -> prop. type std.string.map.find string -> std.string.map A -> A -> prop. type std.string.map.fold std.string.map A -> C -> (string -> A -> C -> C -> prop) -> C -> prop. type std.string.map.map std.string.map A -> (string -> A -> B -> prop) -> std.string.map B -> prop. type std.string.map.mem string -> std.string.map A -> prop. type std.string.map.remove string -> std.string.map A -> std.string.map A -> prop. type std.string.set.add string -> std.string.set -> std.string.set -> prop. type std.string.set.cardinal std.string.set -> int -> prop. type std.string.set.choose std.string.set -> string -> prop. type std.string.set.diff std.string.set -> std.string.set -> std.string.set -> prop. type std.string.set.elements std.string.set -> list string -> prop. type std.string.set.empty std.string.set -> prop. type std.string.set.equal std.string.set -> std.string.set -> prop. type std.string.set.filter std.string.set -> (string -> prop) -> std.string.set -> prop. type std.string.set.fold std.string.set -> A -> (string -> A -> A -> prop) -> A -> prop. type std.string.set.inter std.string.set -> std.string.set -> std.string.set -> prop. type std.string.set.map std.string.set -> (string -> string -> prop) -> std.string.set -> prop. type std.string.set.max std.string.set -> string -> prop. type std.string.set.mem string -> std.string.set -> prop. type std.string.set.min std.string.set -> string -> prop. type std.string.set.partition std.string.set -> (string -> prop) -> std.string.set -> std.string.set -> prop. type std.string.set.remove string -> std.string.set -> std.string.set -> prop. type std.string.set.subset std.string.set -> std.string.set -> prop. type std.string.set.union std.string.set -> std.string.set -> std.string.set -> prop. type std.take int -> list A -> list A -> prop. type std.take-last int -> list A -> list A -> prop. type std.time prop -> float -> prop. type std.unsafe-cast A -> B -> prop. type std.unzip list (pair A B) -> list A -> list B -> prop. type std.while-ok-do! diagnostic -> list (diagnostic -> prop) -> diagnostic -> prop. type std.zip list A -> list B -> list (pair A B) -> prop. type std_err out_stream. type std_in in_stream. type std_out out_stream. type stop prop. type str string -> argument. type string_to_int string -> int. type submodule modpath -> list module-item -> module-item. type substring string -> int -> int -> string. type system string -> int -> prop. type tac ltac1-tactic -> argument. type tc-instance gref -> int -> tc-instance. type term_to_string any -> string -> prop. type trace.counter string -> int -> prop. type triple A -> B -> C -> triple A B C. type triple_1 triple A B C -> A -> prop. type triple_2 triple A B C -> B -> prop. type triple_3 triple A B C -> C -> prop. type trm term -> argument. type true prop. type truncate float -> int. type tt bool. type typ univ -> sort. type uint63 uint63 -> primitive-value. type unix.process out_stream -> in_stream -> in_stream -> unix.process. type unix.process.close unix.process -> diagnostic -> prop. type unix.process.open string -> list string -> list string -> unix.process -> diagnostic -> prop. type upoly-const-decl id -> option term -> arity -> upoly-decl -> argument. type upoly-decl list univ.variable -> bool -> list univ-constraint -> bool -> upoly-decl. type upoly-decl-cumul list univ-variance -> bool -> list univ-constraint -> bool -> upoly-decl-cumul. type upoly-indt-decl indt-decl -> upoly-decl -> argument. type upoly-indt-decl indt-decl -> upoly-decl-cumul -> argument. type usage prop. type uvar A. type uvar evarkey -> list term -> term. type var any -> any ..-> prop. type whd term -> term -> prop. type when list int -> option int -> simplification_strategy. type when-nomatch list int -> option int -> simplification_strategy. type (~) int -> int. type (~) float -> float. typeabbrv field-attributes (list field-attribute). typeabbrv goal-ctx (list prop). typeabbrv id (string). typeabbrv opaque? (bool). % File "elpi-builtin.elpi", line 11, column 0, characters 147-151: [1] true :- . % File "elpi-builtin.elpi", line 34, column 0, characters 373-385: [2] A0 ; _ :- A0. % File "elpi-builtin.elpi", line 36, column 0, characters 388-400: [3] _ ; A0 :- A0. % File "elpi-builtin.elpi", line 62, column 0, characters 759-778: [4] not A0 :- A0, !, fail. % File "elpi-builtin.elpi", line 64, column 0, characters 781-786: [5] not _ :- . % File "elpi-builtin.elpi", line 77, column 0, characters 1124-1136: [6] stop :- halt. % File "elpi-builtin.elpi", line 83, column 0, characters 1181-1199: [7] A1 is A0 :- calc A0 A1. % File "elpi-builtin.elpi", line 182, column 0, characters 2993-3009: [8] A0 > A1 :- gt_ A0 A1. % File "elpi-builtin.elpi", line 185, column 0, characters 3031-3047: [9] A0 < A1 :- lt_ A0 A1. % File "elpi-builtin.elpi", line 188, column 0, characters 3070-3087: [10] A0 =< A1 :- le_ A0 A1. % File "elpi-builtin.elpi", line 191, column 0, characters 3110-3127: [11] A0 >= A1 :- ge_ A0 A1. % File "elpi-builtin.elpi", line 194, column 0, characters 3154-3171: [12] A0 i> A1 :- gt_ A0 A1. % File "elpi-builtin.elpi", line 197, column 0, characters 3198-3215: [13] A0 i< A1 :- lt_ A0 A1. % File "elpi-builtin.elpi", line 200, column 0, characters 3243-3261: [14] A0 i=< A1 :- le_ A0 A1. % File "elpi-builtin.elpi", line 203, column 0, characters 3289-3307: [15] A0 i>= A1 :- ge_ A0 A1. % File "elpi-builtin.elpi", line 206, column 0, characters 3338-3355: [16] A0 r> A1 :- gt_ A0 A1. % File "elpi-builtin.elpi", line 209, column 0, characters 3386-3403: [17] A0 r< A1 :- lt_ A0 A1. % File "elpi-builtin.elpi", line 212, column 0, characters 3435-3453: [18] A0 r=< A1 :- le_ A0 A1. % File "elpi-builtin.elpi", line 215, column 0, characters 3485-3503: [19] A0 r>= A1 :- ge_ A0 A1. % File "elpi-builtin.elpi", line 218, column 0, characters 3536-3553: [20] A0 s> A1 :- gt_ A0 A1. % File "elpi-builtin.elpi", line 221, column 0, characters 3586-3603: [21] A0 s< A1 :- lt_ A0 A1. % File "elpi-builtin.elpi", line 224, column 0, characters 3637-3655: [22] A0 s=< A1 :- le_ A0 A1. % File "elpi-builtin.elpi", line 227, column 0, characters 3689-3707: [23] A0 s>= A1 :- ge_ A0 A1. % File "elpi-builtin.elpi", line 248, column 0, characters 4099-4113: [24] fst (pr A0 _) A0 :- . % File "elpi-builtin.elpi", line 252, column 0, characters 4144-4158: [25] snd (pr _ A0) A0 :- . % File "elpi-builtin.elpi", line 259, column 0, characters 4281-4306: [26] triple_1 (triple A0 _ _) A0 :- . % File "elpi-builtin.elpi", line 262, column 0, characters 4344-4369: [27] triple_2 (triple _ A0 _) A0 :- . % File "elpi-builtin.elpi", line 265, column 0, characters 4407-4432: [28] triple_3 (triple _ _ A0) A0 :- . % File "elpi-builtin.elpi", line 295, column 0, characters 5059-5091: [29] counter A0 A1 :- trace.counter A0 A1. % File "elpi-builtin.elpi", line 321, column 0, characters 5969-6001: [30] rex_match A0 A1 :- rex.match A0 A1. % File "elpi-builtin.elpi", line 325, column 0, characters 6091-6135: [31] rex_replace A0 A1 A2 A3 :- rex.replace A0 A1 A2 A3. % File "elpi-builtin.elpi", line 329, column 0, characters 6216-6252: [32] rex_split A0 A1 A2 :- rex.split A0 A1 A2. % File "elpi-builtin.elpi", line 359, column 0, characters 7377-7400: [33] A0 == A1 :- same_term A0 A1. % File "elpi-builtin.elpi", line 392, column 0, characters 8555-8585: [34] primitive? A0 A1 :- is_cdata A0 A1. % File "elpi-builtin.elpi", line 422, column 0, characters 9560-9579: [35] if A0 A1 _ :- A0, !, A1. % File "elpi-builtin.elpi", line 423, column 0, characters 9581-9594: [36] if _ _ A0 :- A0. % File "elpi-builtin.elpi", line 427, column 0, characters 9724-9754: [37] if2 A0 A1 _ _ _ :- A0, !, A1. % File "elpi-builtin.elpi", line 428, column 0, characters 9756-9786: [38] if2 _ _ A0 A1 _ :- A0, !, A1. % File "elpi-builtin.elpi", line 429, column 0, characters 9788-9813: [39] if2 _ _ _ _ A0 :- !, A0. % File "builtin_stdlib.elpi", line 17, column 0, characters 659-714: [40] default-fatal-error std.fatal-error A0 :- halt A0. % File "builtin_stdlib.elpi", line 21, column 0, characters 756-839: [41] default-fatal-error-w-data std.fatal-error-w-data A0 A1 :- halt A0 : A1. % File "builtin_stdlib.elpi", line 25, column 0, characters 874-940: [42] default-debug-print std.debug-print A0 A1 :- print A0 A1. % File "builtin_stdlib.elpi", line 31, column 0, characters 1007-1032: [43] std.ignore-failure! A0 :- A0, !. % File "builtin_stdlib.elpi", line 32, column 0, characters 1034-1051: [44] std.ignore-failure! _ :- . % File "builtin_stdlib.elpi", line 35, column 0, characters 1072-1086: [45] std.once A0 :- A0, !. % File "builtin_stdlib.elpi", line 39, column 0, characters 1190-1249: [46] std.assert! A0 A1 :- A0 ; std.fatal-error-w-data A1 A0, !. % File "builtin_stdlib.elpi", line 44, column 0, characters 1440-1552: [47] std.assert-ok! A1 A3 :- A1 A0, !, A0 = ok ; A0 = error A2 , std.fatal-error-w-data A3 A2, !. % File "builtin_stdlib.elpi", line 45, column 0, characters 1554-1621: [48] std.assert-ok! _ A0 :- std.fatal-error-w-data A0 no diagnostic returned. % File "builtin_stdlib.elpi", line 49, column 0, characters 1716-1895: [49] std.spy A1 :- trace.counter run A0, if (not (A0 = 0)) (std.debug-print run= A0) true, std.debug-print ----<<---- enter: A1, A1, std.debug-print ---->>---- exit: A1. % File "builtin_stdlib.elpi", line 53, column 0, characters 1897-1945: [50] std.spy A0 :- std.debug-print ---->>---- fail: A0, fail. % File "builtin_stdlib.elpi", line 57, column 0, characters 2035-2218: [51] std.spy! A1 :- trace.counter run A0, if (not (A0 = 0)) (std.debug-print run= A0) true, std.debug-print ----<<---- enter: A1, A1, std.debug-print ---->>---- exit: A1, !. % File "builtin_stdlib.elpi", line 61, column 0, characters 2220-2269: [52] std.spy! A0 :- std.debug-print ---->>---- fail: A0, fail. % File "builtin_stdlib.elpi", line 65, column 0, characters 2329-2353: [53] std.unsafe-cast A0 A0 :- . % File "builtin_stdlib.elpi", line 70, column 0, characters 2410-2452: [54] std.length [_ | A0] A2 :- std.length A0 A1, A2 is A1 + 1. % File "builtin_stdlib.elpi", line 71, column 0, characters 2454-2468: [55] std.length [] 0 :- . % File "builtin_stdlib.elpi", line 74, column 0, characters 2500-2529: [56] std.rev A0 A1 :- std.rev.aux A0 [] A1. % File "builtin_stdlib.elpi", line 77, column 0, characters 2575-2619: [57] std.rev.aux [A1 | A0] A2 A3 :- std.rev.aux A0 [A1 | A2] A3. % File "builtin_stdlib.elpi", line 78, column 0, characters 2621-2635: [58] std.rev.aux [] A0 A0 :- . % File "builtin_stdlib.elpi", line 81, column 0, characters 2663-2708: [59] std.last [] _ :- std.fatal-error last on empty list. % File "builtin_stdlib.elpi", line 82, column 0, characters 2710-2725: [60] std.last [A0] A0 :- !. % File "builtin_stdlib.elpi", line 83, column 0, characters 2727-2753: [61] std.last [_ | A0] A1 :- std.last A0 A1. % File "builtin_stdlib.elpi", line 86, column 0, characters 2798-2838: [62] std.append [A3 | A0] A1 [A3 | A2] :- std.append A0 A1 A2. % File "builtin_stdlib.elpi", line 87, column 0, characters 2841-2854: [63] std.append [] A0 A0 :- . % File "builtin_stdlib.elpi", line 90, column 0, characters 2901-2915: [64] std.appendR [] A0 A0 :- . % File "builtin_stdlib.elpi", line 91, column 0, characters 2917-2959: [65] std.appendR [A3 | A0] A1 [A3 | A2] :- std.appendR A0 A1 A2. % File "builtin_stdlib.elpi", line 94, column 0, characters 2999-3015: [66] std.take 0 _ [] :- !. % File "builtin_stdlib.elpi", line 95, column 0, characters 3017-3068: [67] std.take A1 [A4 | A2] [A4 | A3] :- !, A0 is A1 - 1, std.take A0 A2 A3. % File "builtin_stdlib.elpi", line 96, column 0, characters 3070-3124: [68] std.take _ _ _ :- std.fatal-error take run out of list items. % File "builtin_stdlib.elpi", line 99, column 0, characters 3169-3228: [69] std.take-last A3 A0 A4 :- std.length A0 A1, A2 is A1 - A3, std.drop A2 A0 A4. % File "builtin_stdlib.elpi", line 105, column 0, characters 3268-3283: [70] std.drop 0 A0 A0 :- !. % File "builtin_stdlib.elpi", line 106, column 0, characters 3285-3332: [71] std.drop A1 [_ | A2] A3 :- !, A0 is A1 - 1, std.drop A0 A2 A3. % File "builtin_stdlib.elpi", line 107, column 0, characters 3334-3388: [72] std.drop _ _ _ :- std.fatal-error drop run out of list items. % File "builtin_stdlib.elpi", line 110, column 0, characters 3433-3488: [73] std.drop-last A3 A0 A4 :- std.length A0 A1, A2 is A1 - A3, std.take A2 A0 A4. % File "builtin_stdlib.elpi", line 114, column 0, characters 3542-3564: [74] std.split-at 0 A0 [] A0 :- !. % File "builtin_stdlib.elpi", line 115, column 0, characters 3566-3633: [75] std.split-at A1 [A5 | A2] [A5 | A3] A4 :- !, A0 is A1 - 1, std.split-at A0 A2 A3 A4. % File "builtin_stdlib.elpi", line 116, column 0, characters 3635-3699: [76] std.split-at _ _ _ _ :- std.fatal-error split-at run out of list items. % File "builtin_stdlib.elpi", line 119, column 0, characters 3756-3769: [77] std.fold [] A0 _ A0 :- . % File "builtin_stdlib.elpi", line 120, column 0, characters 3771-3816: [78] std.fold [A0 | A4] A1 A3 A5 :- A3 A0 A1 A2, std.fold A4 A2 A3 A5. % File "builtin_stdlib.elpi", line 123, column 0, characters 3879-3898: [79] std.fold-right [] A0 _ A0 :- . % File "builtin_stdlib.elpi", line 124, column 0, characters 3900-3957: [80] std.fold-right [A4 | A0] A1 A2 A5 :- std.fold-right A0 A1 A2 A3, A2 A4 A3 A5. % File "builtin_stdlib.elpi", line 127, column 0, characters 4030-4102: [81] std.fold2 [] [_ | _] _ _ _ :- std.fatal-error fold2 on lists of different length. % File "builtin_stdlib.elpi", line 128, column 0, characters 4104-4176: [82] std.fold2 [_ | _] [] _ _ _ :- std.fatal-error fold2 on lists of different length. % File "builtin_stdlib.elpi", line 129, column 0, characters 4178-4195: [83] std.fold2 [] [] A0 _ A0 :- . % File "builtin_stdlib.elpi", line 130, column 0, characters 4197-4256: [84] std.fold2 [A0 | A5] [A1 | A6] A2 A4 A7 :- A4 A0 A1 A2 A3, std.fold2 A5 A6 A3 A4 A7. % File "builtin_stdlib.elpi", line 133, column 0, characters 4307-4318: [85] std.map [] _ [] :- . % File "builtin_stdlib.elpi", line 134, column 0, characters 4320-4361: [86] std.map [A0 | A3] A2 [A1 | A4] :- A2 A0 A1, std.map A3 A2 A4. % File "builtin_stdlib.elpi", line 137, column 0, characters 4421-4453: [87] std.map-i A0 A1 A2 :- std.map-i.aux A0 0 A1 A2. % File "builtin_stdlib.elpi", line 140, column 0, characters 4524-4543: [88] std.map-i.aux [] _ _ [] :- . % File "builtin_stdlib.elpi", line 141, column 0, characters 4545-4616: [89] std.map-i.aux [A1 | A5] A0 A3 [A2 | A6] :- A3 A0 A1 A2, A4 is A0 + 1, std.map-i.aux A5 A4 A3 A6. % File "builtin_stdlib.elpi", line 144, column 0, characters 4674-4692: [90] std.map-filter [] _ [] :- . % File "builtin_stdlib.elpi", line 145, column 0, characters 4694-4752: [91] std.map-filter [A0 | A3] A2 [A1 | A4] :- A2 A0 A1, !, std.map-filter A3 A2 A4. % File "builtin_stdlib.elpi", line 146, column 0, characters 4754-4798: [92] std.map-filter [_ | A0] A1 A2 :- std.map-filter A0 A1 A2. % File "builtin_stdlib.elpi", line 150, column 0, characters 4877-4945: [93] std.map2 [] [_ | _] _ _ :- std.fatal-error map2 on lists of different length. % File "builtin_stdlib.elpi", line 151, column 0, characters 4947-5015: [94] std.map2 [_ | _] [] _ _ :- std.fatal-error map2 on lists of different length. % File "builtin_stdlib.elpi", line 152, column 0, characters 5017-5032: [95] std.map2 [] [] _ [] :- . % File "builtin_stdlib.elpi", line 153, column 0, characters 5034-5089: [96] std.map2 [A0 | A4] [A1 | A5] A3 [A2 | A6] :- A3 A0 A1 A2, std.map2 A4 A5 A3 A6. % File "builtin_stdlib.elpi", line 156, column 0, characters 5163-5245: [97] std.map2-filter [] [_ | _] _ _ :- std.fatal-error map2-filter on lists of different length. % File "builtin_stdlib.elpi", line 157, column 0, characters 5247-5329: [98] std.map2-filter [_ | _] [] _ _ :- std.fatal-error map2-filter on lists of different length. % File "builtin_stdlib.elpi", line 158, column 0, characters 5331-5353: [99] std.map2-filter [] [] _ [] :- . % File "builtin_stdlib.elpi", line 159, column 0, characters 5355-5427: [100] std.map2-filter [A0 | A4] [A1 | A5] A3 [A2 | A6] :- A3 A0 A1 A2, !, std.map2-filter A4 A5 A3 A6. % File "builtin_stdlib.elpi", line 160, column 0, characters 5429-5485: [101] std.map2-filter [_ | A0] [_ | A1] A2 A3 :- std.map2-filter A0 A1 A2 A3. % File "builtin_stdlib.elpi", line 163, column 0, characters 5567-5643: [102] std.map-ok [A0 | A4] A3 [A1 | A5] A6 :- A3 A0 A1 A2, if (A2 = ok) (std.map-ok A4 A3 A5 A6) (A6 = A2). % File "builtin_stdlib.elpi", line 164, column 0, characters 5645-5662: [103] std.map-ok [] _ [] ok :- . % File "builtin_stdlib.elpi", line 167, column 0, characters 5738-5758: [104] std.fold-map [] A0 _ [] A0 :- . % File "builtin_stdlib.elpi", line 168, column 0, characters 5760-5827: [105] std.fold-map [A0 | A5] A1 A4 [A2 | A6] A7 :- A4 A0 A1 A2 A3, std.fold-map A5 A3 A4 A6 A7. % File "builtin_stdlib.elpi", line 171, column 0, characters 5883-5899: [106] std.omap none _ none :- . % File "builtin_stdlib.elpi", line 172, column 0, characters 5901-5934: [107] std.omap (some A0) A2 (some A1) :- A2 A0 A1. % File "builtin_stdlib.elpi", line 176, column 0, characters 6041-6067: [108] std.nth 0 [A0 | _] A1 :- !, A0 = A1. % File "builtin_stdlib.elpi", line 177, column 0, characters 6069-6121: [109] std.nth A0 [_ | A2] A3 :- A0 > 0, !, A1 is A0 - 1, std.nth A1 A2 A3. % File "builtin_stdlib.elpi", line 178, column 0, characters 6123-6184: [110] std.nth A0 _ _ :- A0 < 0, !, std.fatal-error nth got a negative index. % File "builtin_stdlib.elpi", line 179, column 0, characters 6186-6238: [111] std.nth _ _ _ :- std.fatal-error nth run out of list items. % File "builtin_stdlib.elpi", line 183, column 0, characters 6327-6348: [112] std.lookup [pr A0 A1 | _] A0 A1 :- . % File "builtin_stdlib.elpi", line 184, column 0, characters 6350-6390: [113] std.lookup [_ | A0] A1 A2 :- std.lookup A0 A1 A2. % File "builtin_stdlib.elpi", line 188, column 0, characters 6509-6536: [114] std.lookup! [pr A0 A1 | _] A0 A1 :- !. % File "builtin_stdlib.elpi", line 189, column 0, characters 6538-6580: [115] std.lookup! [_ | A0] A1 A2 :- std.lookup! A0 A1 A2. % File "builtin_stdlib.elpi", line 193, column 0, characters 6657-6674: [116] std.mem! [A0 | _] A0 :- !. % File "builtin_stdlib.elpi", line 194, column 0, characters 6676-6700: [117] std.mem! [_ | A0] A1 :- std.mem! A0 A1. % File "builtin_stdlib.elpi", line 198, column 0, characters 6781-6792: [118] std.mem [A0 | _] A0 :- . % File "builtin_stdlib.elpi", line 199, column 0, characters 6794-6816: [119] std.mem [_ | A0] A1 :- std.mem A0 A1. % File "builtin_stdlib.elpi", line 202, column 0, characters 6855-6876: [120] std.exists [A0 | _] A1 :- A1 A0. % File "builtin_stdlib.elpi", line 203, column 0, characters 6878-6906: [121] std.exists [_ | A0] A1 :- std.exists A0 A1. % File "builtin_stdlib.elpi", line 206, column 0, characters 6961-7033: [122] std.exists2 [] [_ | _] _ :- std.fatal-error exists2 on lists of different length. % File "builtin_stdlib.elpi", line 207, column 0, characters 7035-7107: [123] std.exists2 [_ | _] [] _ :- std.fatal-error exists2 on lists of different length. % File "builtin_stdlib.elpi", line 208, column 0, characters 7109-7139: [124] std.exists2 [A0 | _] [A1 | _] A2 :- A2 A0 A1. % File "builtin_stdlib.elpi", line 209, column 0, characters 7141-7179: [125] std.exists2 [_ | A0] [_ | A1] A2 :- std.exists2 A0 A1 A2. % File "builtin_stdlib.elpi", line 212, column 0, characters 7218-7229: [126] std.forall [] _ :- . % File "builtin_stdlib.elpi", line 213, column 0, characters 7231-7264: [127] std.forall [A0 | A2] A1 :- A1 A0, std.forall A2 A1. % File "builtin_stdlib.elpi", line 216, column 0, characters 7334-7404: [128] std.forall-ok [A0 | A3] A2 A4 :- A2 A0 A1, if (A1 = ok) (std.forall-ok A3 A2 A4) (A4 = A1). % File "builtin_stdlib.elpi", line 217, column 0, characters 7406-7423: [129] std.forall-ok [] _ ok :- . % File "builtin_stdlib.elpi", line 220, column 0, characters 7478-7550: [130] std.forall2 [] [_ | _] _ :- std.fatal-error forall2 on lists of different length. % File "builtin_stdlib.elpi", line 221, column 0, characters 7552-7624: [131] std.forall2 [_ | _] [] _ :- std.fatal-error forall2 on lists of different length. % File "builtin_stdlib.elpi", line 222, column 0, characters 7626-7675: [132] std.forall2 [A0 | A3] [A1 | A4] A2 :- A2 A0 A1, std.forall2 A3 A4 A2. % File "builtin_stdlib.elpi", line 223, column 0, characters 7677-7692: [133] std.forall2 [] [] _ :- . % File "builtin_stdlib.elpi", line 226, column 0, characters 7741-7758: [134] std.filter [] _ [] :- . % File "builtin_stdlib.elpi", line 227, column 0, characters 7760-7826: [135] std.filter [A0 | A4] A1 A2 :- if (A1 A0) (A2 = [A0 | A3]) (A2 = A3), std.filter A4 A1 A3. % File "builtin_stdlib.elpi", line 230, column 0, characters 7877-7941: [136] std.zip [_ | _] [] _ :- std.fatal-error zip on lists of different length. % File "builtin_stdlib.elpi", line 231, column 0, characters 7943-8007: [137] std.zip [] [_ | _] _ :- std.fatal-error zip on lists of different length. % File "builtin_stdlib.elpi", line 232, column 0, characters 8009-8054: [138] std.zip [A3 | A0] [A4 | A1] [pr A3 A4 | A2] :- std.zip A0 A1 A2. % File "builtin_stdlib.elpi", line 233, column 0, characters 8056-8068: [139] std.zip [] [] [] :- . % File "builtin_stdlib.elpi", line 236, column 0, characters 8121-8135: [140] std.unzip [] [] [] :- . % File "builtin_stdlib.elpi", line 237, column 0, characters 8137-8184: [141] std.unzip [pr A3 A4 | A0] [A3 | A1] [A4 | A2] :- std.unzip A0 A1 A2. % File "builtin_stdlib.elpi", line 240, column 0, characters 8227-8277: [142] std.flatten [A2 | A0] A3 :- std.flatten A0 A1, std.append A2 A1 A3. % File "builtin_stdlib.elpi", line 241, column 0, characters 8279-8296: [143] std.flatten [] [] :- . % File "builtin_stdlib.elpi", line 244, column 0, characters 8319-8326: [144] std.null [] :- . % File "builtin_stdlib.elpi", line 248, column 0, characters 8417-8438: [145] std.list.make 0 _ [] :- !. % File "builtin_stdlib.elpi", line 249, column 0, characters 8440-8492: [146] std.list.make A1 A2 [A2 | A3] :- A0 is A1 - 1, std.list.make A0 A2 A3. % File "builtin_stdlib.elpi", line 253, column 0, characters 8588-8628: [147] std.list.init A0 A1 A2 :- std.list.init.aux 0 A0 A1 A2. % File "builtin_stdlib.elpi", line 256, column 0, characters 8695-8722: [148] std.list.init.aux A0 A0 _ [] :- !. % File "builtin_stdlib.elpi", line 257, column 0, characters 8724-8795: [149] std.list.init.aux A0 A4 A2 [A1 | A5] :- A2 A0 A1, A3 is A0 + 1, std.list.init.aux A3 A4 A2 A5. % File "builtin_stdlib.elpi", line 260, column 0, characters 8827-8865: [150] std.iota A0 A1 :- std.list.init A0 (c0 \ c1 \ c0 = c1) A1. % File "builtin_stdlib.elpi", line 265, column 0, characters 8969-8988: [151] std.intersperse _ [] [] :- . % File "builtin_stdlib.elpi", line 266, column 0, characters 8990-9016: [152] std.intersperse _ [A0] [A0] :- !. % File "builtin_stdlib.elpi", line 267, column 0, characters 9018-9076: [153] std.intersperse A0 [A3 | A1] [A3, A0 | A2] :- std.intersperse A0 A1 A2. % File "builtin_stdlib.elpi", line 272, column 0, characters 9133-9152: [154] std.flip A2 A1 A0 :- A2 A0 A1. % File "builtin_stdlib.elpi", line 275, column 0, characters 9182-9257: [155] std.time A1 A3 :- gettimeofday A0, A1, gettimeofday A2, A3 is A2 - A0. % File "builtin_stdlib.elpi", line 278, column 0, characters 9282-9288: [156] std.do! [] :- . % File "builtin_stdlib.elpi", line 279, column 0, characters 9290-9316: [157] std.do! [A0 | A1] :- A0, !, std.do! A1. % File "builtin_stdlib.elpi", line 283, column 0, characters 9385-9397: [158] std.do-ok! ok [] :- . % File "builtin_stdlib.elpi", line 284, column 0, characters 9399-9462: [159] std.do-ok! A2 [A1 | A3] :- A1 A0, !, if (A0 = ok) (std.do-ok! A2 A3) (A2 = A0). % File "builtin_stdlib.elpi", line 287, column 0, characters 9510-9555: [160] std.lift-ok A0 A2 A1 :- A0 , A1 = ok ; A1 = error A2. % File "builtin_stdlib.elpi", line 290, column 0, characters 9584-9629: [161] std.spy-do! A0 :- std.map A0 (c0 \ c1 \ c1 = std.spy c0) A1, std.do! A1. % File "builtin_stdlib.elpi", line 293, column 0, characters 9706-9737: [162] std.while-ok-do! (as (error _) A0) _ A0 :- . % File "builtin_stdlib.elpi", line 294, column 0, characters 9739-9760: [163] std.while-ok-do! ok [] ok :- . % File "builtin_stdlib.elpi", line 295, column 0, characters 9762-9817: [164] std.while-ok-do! ok [A1 | A2] A3 :- A1 A0, !, std.while-ok-do! A0 A2 A3. % File "builtin_stdlib.elpi", line 298, column 0, characters 9852-9889: [165] std.any->string A0 A1 :- term_to_string A0 A1. % File "builtin_stdlib.elpi", line 301, column 0, characters 9916-9938: [166] std.max A0 A1 A0 :- A0 >= A1, !. % File "builtin_stdlib.elpi", line 302, column 0, characters 9940-9949: [167] std.max _ A0 A0 :- . % File "builtin_stdlib.elpi", line 306, column 0, characters 10063-10099: [168] std.findall A0 A1 :- findall_solutions A0 A1. % File "builtin_map.elpi", line 8, column 0, characters 10432-10468: [169] std.map.make A0 (std.map std.map.private.empty A0) :- . % File "builtin_map.elpi", line 12, column 0, characters 10564-10614: [170] std.map.find A2 (std.map A0 A1) A3 :- std.map.private.find A0 A1 A2 A3. % File "builtin_map.elpi", line 16, column 0, characters 10713-10781: [171] std.map.add A2 A3 (std.map A0 A1) (std.map A4 A1) :- std.map.private.add A0 A1 A2 A3 A4. % File "builtin_map.elpi", line 20, column 0, characters 10876-10946: [172] std.map.remove A2 (std.map A0 A1) (std.map A3 A1) :- std.map.private.remove A0 A1 A2 A3. % File "builtin_map.elpi", line 24, column 0, characters 11059-11110: [173] std.map.bindings (std.map A0 _) A1 :- std.map.private.bindings A0 [] A1. % File "builtin_map.elpi", line 34, column 0, characters 11302-11316: [174] std.map.private.height std.map.private.empty 0 :- . % File "builtin_map.elpi", line 35, column 0, characters 11318-11343: [175] std.map.private.height (std.map.private.node _ _ _ _ A0) A0 :- . % File "builtin_map.elpi", line 38, column 0, characters 11401-11476: [176] std.map.private.create A0 A6 A7 A2 (std.map.private.node A0 A6 A7 A2 A5) :- std.map.private.height A0 A1, std.map.private.height A2 A3, std.max A1 A3 A4, A5 is A4 + 1. % File "builtin_map.elpi", line 41, column 0, characters 11531-11645: [177] std.map.private.bal A0 A6 A7 A2 A8 :- std.map.private.height A0 A1, std.map.private.height A2 A3, A4 is A1 + 2, A5 is A3 + 2, std.map.private.bal.aux A1 A3 A4 A5 A0 A6 A7 A2 A8. % File "builtin_map.elpi", line 49, column 0, characters 11732-11863: [178] std.map.private.bal.aux A0 _ _ A1 (std.map.private.node A2 A10 A11 A4 _) A6 A7 A8 A12 :- A0 > A1, std.map.private.height A2 A3, std.map.private.height A4 A5, A3 >= A5, !, std.map.private.create A4 A6 A7 A8 A9, std.map.private.create A2 A10 A11 A9 A12. % File "builtin_map.elpi", line 52, column 0, characters 11865-12012: [179] std.map.private.bal.aux A0 _ _ A1 (std.map.private.node A2 A3 A4 (std.map.private.node A5 A12 A13 A7 _) _) A8 A9 A10 A14 :- A0 > A1, !, std.map.private.create A2 A3 A4 A5 A6, std.map.private.create A7 A8 A9 A10 A11, std.map.private.create A6 A12 A13 A11 A14. % File "builtin_map.elpi", line 55, column 0, characters 12014-12145: [180] std.map.private.bal.aux _ A0 A1 _ A6 A7 A8 (std.map.private.node A4 A10 A11 A2 _) A12 :- A0 > A1, std.map.private.height A2 A3, std.map.private.height A4 A5, A3 >= A5, !, std.map.private.create A6 A7 A8 A4 A9, std.map.private.create A9 A10 A11 A2 A12. % File "builtin_map.elpi", line 58, column 0, characters 12147-12294: [181] std.map.private.bal.aux _ A0 A1 _ A2 A3 A4 (std.map.private.node (std.map.private.node A5 A12 A13 A7 _) A8 A9 A10 _) A14 :- A0 > A1, !, std.map.private.create A2 A3 A4 A5 A6, std.map.private.create A7 A8 A9 A10 A11, std.map.private.create A6 A12 A13 A11 A14. % File "builtin_map.elpi", line 61, column 0, characters 12296-12341: [182] std.map.private.bal.aux _ _ _ _ A0 A1 A2 A3 A4 :- std.map.private.create A0 A1 A2 A3 A4. % File "builtin_map.elpi", line 64, column 0, characters 12411-12456: [183] std.map.private.add std.map.private.empty _ A0 A1 A2 :- std.map.private.create std.map.private.empty A0 A1 std.map.private.empty A2. % File "builtin_map.elpi", line 65, column 0, characters 12458-12536: [184] std.map.private.add (as (std.map.private.node _ A1 _ _ _) A4) A3 A0 A5 A6 :- A3 A0 A1 A2, std.map.private.add.aux A2 A4 A3 A0 A5 A6. % File "builtin_map.elpi", line 68, column 0, characters 12617-12678: [185] std.map.private.add.aux eq (std.map.private.node A1 _ _ A4 A5) _ A2 A3 A0 :- A0 = std.map.private.node A1 A2 A3 A4 A5. % File "builtin_map.elpi", line 69, column 0, characters 12681-12751: [186] std.map.private.add.aux lt (std.map.private.node A0 A5 A6 A7 _) A1 A2 A3 A8 :- std.map.private.add A0 A1 A2 A3 A4, std.map.private.bal A4 A5 A6 A7 A8. % File "builtin_map.elpi", line 70, column 0, characters 12753-12823: [187] std.map.private.add.aux gt (std.map.private.node A5 A6 A7 A0 _) A1 A2 A3 A8 :- std.map.private.add A0 A1 A2 A3 A4, std.map.private.bal A5 A6 A7 A4 A8. % File "builtin_map.elpi", line 73, column 0, characters 12883-12955: [188] std.map.private.find (std.map.private.node A4 A1 A6 A5 _) A3 A0 A7 :- A3 A0 A1 A2, std.map.private.find.aux A2 A3 A4 A5 A6 A0 A7. % File "builtin_map.elpi", line 76, column 0, characters 13042-13067: [189] std.map.private.find.aux eq _ _ _ A0 _ A0 :- . % File "builtin_map.elpi", line 77, column 0, characters 13069-13112: [190] std.map.private.find.aux lt A1 A0 _ _ A2 A3 :- std.map.private.find A0 A1 A2 A3. % File "builtin_map.elpi", line 78, column 0, characters 13114-13157: [191] std.map.private.find.aux gt A1 _ A0 _ A2 A3 :- std.map.private.find A0 A1 A2 A3. % File "builtin_map.elpi", line 81, column 0, characters 13206-13252: [192] std.map.private.remove-min-binding (std.map.private.node std.map.private.empty _ _ A0 _) A0 :- !. % File "builtin_map.elpi", line 82, column 0, characters 13254-13329: [193] std.map.private.remove-min-binding (std.map.private.node A0 A2 A3 A4 _) A5 :- std.map.private.remove-min-binding A0 A1, std.map.private.bal A1 A2 A3 A4 A5. % File "builtin_map.elpi", line 85, column 0, characters 13370-13411: [194] std.map.private.min-binding (std.map.private.node std.map.private.empty A0 A1 _ _) A0 A1 :- !. % File "builtin_map.elpi", line 86, column 0, characters 13413-13466: [195] std.map.private.min-binding (std.map.private.node A0 _ _ _ _) A1 A2 :- std.map.private.min-binding A0 A1 A2. % File "builtin_map.elpi", line 89, column 0, characters 13513-13533: [196] std.map.private.merge std.map.private.empty A0 A0 :- !. % File "builtin_map.elpi", line 90, column 0, characters 13535-13555: [197] std.map.private.merge A0 std.map.private.empty A0 :- !. % File "builtin_map.elpi", line 91, column 0, characters 13557-13634: [198] std.map.private.merge A4 A0 A5 :- std.map.private.min-binding A0 A1 A2, std.map.private.remove-min-binding A0 A3, std.map.private.bal A4 A1 A2 A3 A5. % File "builtin_map.elpi", line 96, column 0, characters 13702-13729: [199] std.map.private.remove std.map.private.empty _ _ std.map.private.empty :- !. % File "builtin_map.elpi", line 97, column 0, characters 13731-13805: [200] std.map.private.remove (std.map.private.node A4 A1 A6 A5 _) A3 A0 A7 :- A3 A0 A1 A2, std.map.private.remove.aux A2 A3 A4 A5 A1 A6 A0 A7. % File "builtin_map.elpi", line 100, column 0, characters 13905-13949: [201] std.map.private.remove.aux eq _ A0 A1 _ _ _ A2 :- std.map.private.merge A0 A1 A2. % File "builtin_map.elpi", line 101, column 0, characters 13951-14012: [202] std.map.private.remove.aux lt A1 A0 A6 A4 A5 A2 A7 :- std.map.private.remove A0 A1 A2 A3, std.map.private.bal A3 A4 A5 A6 A7. % File "builtin_map.elpi", line 102, column 0, characters 14014-14075: [203] std.map.private.remove.aux gt A1 A4 A0 A5 A6 A2 A7 :- std.map.private.remove A0 A1 A2 A3, std.map.private.bal A4 A5 A6 A3 A7. % File "builtin_map.elpi", line 105, column 0, characters 14141-14159: [204] std.map.private.bindings std.map.private.empty A0 A0 :- . % File "builtin_map.elpi", line 106, column 0, characters 14161-14234: [205] std.map.private.bindings (std.map.private.node A3 A4 A5 A0 _) A1 A6 :- std.map.private.bindings A0 A1 A2, std.map.private.bindings A3 [pr A4 A5 | A2] A6. % File "builtin_set.elpi", line 8, column 0, characters 22779-22815: [206] std.set.make A0 (std.set std.set.private.empty A0) :- . % File "builtin_set.elpi", line 12, column 0, characters 22876-22919: [207] std.set.mem A2 (std.set A0 A1) :- std.set.private.mem A0 A1 A2. % File "builtin_set.elpi", line 16, column 0, characters 22991-23055: [208] std.set.add A2 (std.set A0 A1) (std.set A3 A1) :- std.set.private.add A0 A1 A2 A3. % File "builtin_set.elpi", line 20, column 0, characters 23133-23203: [209] std.set.remove A2 (std.set A0 A1) (std.set A3 A1) :- std.set.private.remove A0 A1 A2 A3. % File "builtin_set.elpi", line 24, column 0, characters 23290-23338: [210] std.set.cardinal (std.set A0 _) A1 :- std.set.private.cardinal A0 A1. % File "builtin_set.elpi", line 27, column 0, characters 23378-23429: [211] std.set.elements (std.set A0 _) A1 :- std.set.private.elements A0 [] A1. % File "builtin_set.elpi", line 37, column 0, characters 23598-23612: [212] std.set.private.height std.set.private.empty 0 :- . % File "builtin_set.elpi", line 38, column 0, characters 23614-23637: [213] std.set.private.height (std.set.private.node _ _ _ A0) A0 :- . % File "builtin_set.elpi", line 41, column 0, characters 23684-23755: [214] std.set.private.create A0 A6 A2 (std.set.private.node A0 A6 A2 A5) :- std.set.private.height A0 A1, std.set.private.height A2 A3, std.max A1 A3 A4, A5 is A4 + 1. % File "builtin_set.elpi", line 44, column 0, characters 23799-23909: [215] std.set.private.bal A0 A6 A2 A7 :- std.set.private.height A0 A1, std.set.private.height A2 A3, A4 is A1 + 2, A5 is A3 + 2, std.set.private.bal.aux A1 A3 A4 A5 A0 A6 A2 A7. % File "builtin_set.elpi", line 52, column 0, characters 23985-24106: [216] std.set.private.bal.aux A0 _ _ A1 (std.set.private.node A2 A9 A4 _) A6 A7 A10 :- A0 > A1, std.set.private.height A2 A3, std.set.private.height A4 A5, A3 >= A5, !, std.set.private.create A4 A6 A7 A8, std.set.private.create A2 A9 A8 A10. % File "builtin_set.elpi", line 55, column 0, characters 24108-24237: [217] std.set.private.bal.aux A0 _ _ A1 (std.set.private.node A2 A3 (std.set.private.node A4 A10 A6 _) _) A7 A8 A11 :- A0 > A1, !, std.set.private.create A2 A3 A4 A5, std.set.private.create A6 A7 A8 A9, std.set.private.create A5 A10 A9 A11. % File "builtin_set.elpi", line 58, column 0, characters 24239-24360: [218] std.set.private.bal.aux _ A0 A1 _ A6 A7 (std.set.private.node A4 A9 A2 _) A10 :- A0 > A1, std.set.private.height A2 A3, std.set.private.height A4 A5, A3 >= A5, !, std.set.private.create A6 A7 A4 A8, std.set.private.create A8 A9 A2 A10. % File "builtin_set.elpi", line 61, column 0, characters 24362-24491: [219] std.set.private.bal.aux _ A0 A1 _ A2 A3 (std.set.private.node (std.set.private.node A4 A10 A6 _) A7 A8 _) A11 :- A0 > A1, !, std.set.private.create A2 A3 A4 A5, std.set.private.create A6 A7 A8 A9, std.set.private.create A5 A10 A9 A11. % File "builtin_set.elpi", line 64, column 0, characters 24493-24534: [220] std.set.private.bal.aux _ _ _ _ A0 A1 A2 A3 :- std.set.private.create A0 A1 A2 A3. % File "builtin_set.elpi", line 67, column 0, characters 24595-24636: [221] std.set.private.add std.set.private.empty _ A0 A1 :- std.set.private.create std.set.private.empty A0 std.set.private.empty A1. % File "builtin_set.elpi", line 68, column 0, characters 24638-24707: [222] std.set.private.add (std.set.private.node A4 A1 A5 A6) A3 A0 A7 :- A3 A0 A1 A2, std.set.private.add.aux A2 A3 A4 A5 A1 A0 A6 A7. % File "builtin_set.elpi", line 71, column 0, characters 24800-24839: [223] std.set.private.add.aux eq _ A0 A1 A2 _ A3 (std.set.private.node A0 A2 A1 A3) :- . % File "builtin_set.elpi", line 72, column 0, characters 24841-24894: [224] std.set.private.add.aux lt A1 A0 A5 A4 A2 _ A6 :- std.set.private.add A0 A1 A2 A3, std.set.private.bal A3 A4 A5 A6. % File "builtin_set.elpi", line 73, column 0, characters 24896-24949: [225] std.set.private.add.aux gt A1 A4 A0 A5 A2 _ A6 :- std.set.private.add A0 A1 A2 A3, std.set.private.bal A4 A5 A3 A6. % File "builtin_set.elpi", line 76, column 0, characters 25001-25059: [226] std.set.private.mem (std.set.private.node A4 A1 A5 _) A3 A0 :- A3 A0 A1 A2, std.set.private.mem.aux A2 A3 A4 A5 A0. % File "builtin_set.elpi", line 77, column 0, characters 25061-25079: [227] std.set.private.mem.aux eq _ _ _ _ :- . % File "builtin_set.elpi", line 80, column 0, characters 25151-25186: [228] std.set.private.mem.aux lt A1 A0 _ A2 :- std.set.private.mem A0 A1 A2. % File "builtin_set.elpi", line 81, column 0, characters 25188-25223: [229] std.set.private.mem.aux gt A1 _ A0 A2 :- std.set.private.mem A0 A1 A2. % File "builtin_set.elpi", line 84, column 0, characters 25268-25312: [230] std.set.private.remove-min-binding (std.set.private.node std.set.private.empty _ A0 _) A0 :- !. % File "builtin_set.elpi", line 85, column 0, characters 25314-25385: [231] std.set.private.remove-min-binding (std.set.private.node A0 A2 A3 _) A4 :- std.set.private.remove-min-binding A0 A1, std.set.private.bal A1 A2 A3 A4. % File "builtin_set.elpi", line 88, column 0, characters 25419-25456: [232] std.set.private.min-binding (std.set.private.node std.set.private.empty A0 _ _) A0 :- !. % File "builtin_set.elpi", line 89, column 0, characters 25458-25505: [233] std.set.private.min-binding (std.set.private.node A0 _ _ _) A1 :- std.set.private.min-binding A0 A1. % File "builtin_set.elpi", line 92, column 0, characters 25546-25566: [234] std.set.private.merge std.set.private.empty A0 A0 :- !. % File "builtin_set.elpi", line 93, column 0, characters 25568-25588: [235] std.set.private.merge A0 std.set.private.empty A0 :- !. % File "builtin_set.elpi", line 94, column 0, characters 25590-25663: [236] std.set.private.merge A3 A0 A4 :- std.set.private.min-binding A0 A1, std.set.private.remove-min-binding A0 A2, std.set.private.bal A3 A1 A2 A4. % File "builtin_set.elpi", line 99, column 0, characters 25727-25749: [237] std.set.private.remove std.set.private.empty _ _ std.set.private.empty :- . % File "builtin_set.elpi", line 100, column 0, characters 25751-25821: [238] std.set.private.remove (std.set.private.node A4 A1 A5 _) A3 A0 A6 :- A3 A0 A1 A2, std.set.private.remove.aux A2 A3 A4 A5 A1 A0 A6. % File "builtin_set.elpi", line 103, column 0, characters 25910-25952: [239] std.set.private.remove.aux eq _ A0 A1 _ _ A2 :- std.set.private.merge A0 A1 A2. % File "builtin_set.elpi", line 104, column 0, characters 25954-26011: [240] std.set.private.remove.aux lt A1 A0 A5 A4 A2 A6 :- std.set.private.remove A0 A1 A2 A3, std.set.private.bal A3 A4 A5 A6. % File "builtin_set.elpi", line 105, column 0, characters 26013-26070: [241] std.set.private.remove.aux gt A1 A4 A0 A5 A2 A6 :- std.set.private.remove A0 A1 A2 A3, std.set.private.bal A4 A5 A3 A6. % File "builtin_set.elpi", line 108, column 0, characters 26103-26119: [242] std.set.private.cardinal std.set.private.empty 0 :- . % File "builtin_set.elpi", line 109, column 0, characters 26121-26186: [243] std.set.private.cardinal (std.set.private.node A0 _ A2 _) A4 :- std.set.private.cardinal A0 A1, std.set.private.cardinal A2 A3, A4 is A1 + 1 + A3. % File "builtin_set.elpi", line 112, column 0, characters 26232-26250: [244] std.set.private.elements std.set.private.empty A0 A0 :- . % File "builtin_set.elpi", line 113, column 0, characters 26252-26320: [245] std.set.private.elements (std.set.private.node A3 A4 A0 _) A1 A5 :- std.set.private.elements A0 A1 A2, std.set.private.elements A3 [A4 | A2] A5. % File "builtin_set.elpi", line 255, column 0, characters 31127-31176: [246] printterm A2 A0 :- term_to_string A0 A1, output A2 A1. % File "coq-builtin.elpi", line 270, column 0, characters 10864-10984: [247] default-declare-evar declare-evar A0 A1 A2 A3 :- declare_constraint (declare-evar A0 A1 A2 A3) [A1]. % File "coq-builtin.elpi", line 279, column 0, characters 11224-11299: [248] rm-evar (as uvar A0) (as uvar A1) :- !, declare_constraint (rm-evar A0 A1) [A0, A1]. % File "coq-builtin.elpi", line 280, column 0, characters 11301-11312: [249] rm-evar _ _ :- . % File "coq-builtin.elpi", line 301, column 0, characters 12081-12184: [250] evar (as uvar A3) A2 A0 :- var A0 _ A1, !, prune A2 A1, prune A3 A1, declare_constraint (evar A3 A2 A0) [A3, A0]. % File "coq-builtin.elpi", line 304, column 0, characters 12187-12225: [251] default-assign-evar evar _ _ _ :- . % File "coq-builtin.elpi", line 752, column 2, characters 30724-30883: [252] coq.env.const-opaque? A0 :- coq.warning elpi.deprecated elpi.const-opaque use coq.env.opaque? in place of coq.env.const-opaque?, coq.env.opaque? A0. % File "coq-builtin.elpi", line 759, column 2, characters 30972-31146: [253] coq.env.const-primitive? A0 :- coq.warning elpi.deprecated elpi.const-primitive use coq.env.primitive? in place of coq.env.const-primitive?, coq.env.primitive? A0. % File "coq-builtin.elpi", line 841, column 0, characters 34315-34386: [254] coq.env.begin-module A0 A1 :- coq.env.begin-module-functor A0 A1 []. % File "coq-builtin.elpi", line 854, column 0, characters 34796-34873: [255] coq.env.begin-module-type A0 :- coq.env.begin-module-type-functor A0 []. % File "coq-builtin.elpi", line 1233, column 0, characters 49548-49738: [256] coq.CS.canonical-projections A0 A1 :- coq.warning elpi.deprecated elpi.canonical-projections use coq.env.projections in place of coq.CS.canonical-projections, coq.env.projections A0 A1. % File "coq-builtin.elpi", line 1537, column 0, characters 62306-62486: [257] coq.reduction.cbv.whd_all A0 A1 :- coq.warning elpi.deprecated elpi.cbv-whd-all use coq.reduction.cbv.norm in place of coq.reduction.cbv.whd_all, coq.reduction.cbv.norm A0 A1. % File "coq-builtin.elpi", line 1544, column 0, characters 62584-62765: [258] coq.reduction.vm.whd_all A0 A1 A2 :- coq.warning elpi.deprecated elpi.vm-whd-all use coq.reduction.vm.norm in place of coq.reduction.vm.whd_all, coq.reduction.vm.norm A0 A1 A2. % File "coq-builtin.elpi", line 1551, column 0, characters 62818-62911: [259] coq.reduction.lazy.whd_all A0 A1 :- get-option coq:redflags coq.redflags.all => coq.reduction.lazy.whd A0 A1. % File "coq-builtin.elpi", line 1668, column 0, characters 67289-67329: [260] coq.id->name A0 A1 :- coq.string->name A0 A1. % File "coq-builtin.elpi", line 1770, column 0, characters 71063-71127: [261] coq.elpi.accumulate A0 A1 A2 :- coq.elpi.accumulate-clauses A0 A1 [A2]. % File "./examples/tutorial_elpi_lang.v", line 491, column 2, characters 12652-12720: [262] whd (app A0 A2) A3 :- whd A0 (fun A1), !, whd (A1 A2) A3. % File "./examples/tutorial_elpi_lang.v", line 495, column 2, characters 12775-12801: [263] whd A1 A0 :- A0 = A1. % File "./examples/tutorial_elpi_lang.v", line 591, column 2, characters 15200-15250: [264] of (app A0 A3) A2 :- of A0 (arr A1 A2), of A3 A1. % File "./examples/tutorial_elpi_lang.v", line 596, column 2, characters 15366-15421: [265] of (fun A0) (arr A2 A1) :- pi c0 \ of c0 A2 => of (A0 c0) A1.