Module Ast.Term

type impl_kind =
  1. | L2R
  2. | L2RBang
  3. | R2L
type t_ =
  1. | Impl of impl_kind * Loc.t * t * t
  2. | Const of Scope.t * Name.t
  3. | Discard
  4. | Var of Name.t * Loc.t * t list
    (*

    unification variable

    *)
  5. | App of Scope.t * Name.t * Loc.t * t * t list
  6. | Lam of (Name.t * Loc.t * Scope.language) option * Type.t option * t
  7. | Opaque of Opaque.t
  8. | Cast of t * Type.t
and t = {
  1. it : t_;
  2. loc : Loc.t;
}
val pp : Stdlib.Format.formatter -> t -> unit
val show : t -> string
type constant = Name.constant

See RawData.Constants to allocate global constants

val mkGlobal : loc:Loc.t -> constant -> t
val mkBound : loc:Loc.t -> language:Scope.language -> Name.t -> t
val mkAppGlobal : loc:Loc.t -> hdloc:Loc.t -> constant -> t -> t list -> t
val mkAppBound : loc:Loc.t -> hdloc:Loc.t -> language:Scope.language -> Name.t -> t -> t list -> t
val mkVar : loc:Loc.t -> hdloc:Loc.t -> Name.t -> t list -> t
val mkOpaque : loc:Loc.t -> Opaque.t -> t
val mkCast : loc:Loc.t -> t -> Type.t -> t
val mkLam : loc:Loc.t -> (Name.t * Loc.t * Scope.language) option -> ?ty:Type.t -> t -> t
val mkDiscard : loc:Loc.t -> t
val mkImplication : loc:Loc.t -> hdloc:Loc.t -> t -> t -> t

Handy constructors to build goals

val mkPi : loc:Loc.t -> hdloc:Loc.t -> Name.t -> nloc:Loc.t -> ?ty:Type.t -> t -> t
val mkConj : loc:Loc.t -> hdloc:Loc.t -> t list -> t
val mkEq : loc:Loc.t -> hdloc:Loc.t -> t -> t -> t
val mkNil : loc:Loc.t -> t

if omitted, the loc is the merge of the hd and tl locs, as if one wrote (hd :: tl), but not as if one wrote hd|tl

val mkCons : ?loc:Loc.t -> hdloc:Loc.t -> t -> t -> t

if omitted, the loc is the merge of the hd and tl locs, as if one wrote (hd :: tl), but not as if one wrote hd|tl

val list_to_lp_list : loc:Loc.t -> t list -> t
val ne_list_to_lp_list : t list -> t
val lp_list_to_list : t -> t list
val apply_elpi_var_from_quotation : t -> t list -> t

See Coq-Elpi's lp:(F x) construct

val extend_spill_hyp_from_quotation : t -> t list -> t
val is_spill_from_quotation : t -> bool