package elpi

  1. Overview
  2. Docs
package elpi
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Ast.TermSource

Sourcetype impl_kind =
  1. | L2R
  2. | L2RBang
  3. | R2L
Sourcetype 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
Sourceand t = {
  1. it : t_;
  2. loc : Loc.t;
}
Sourceval pp : Format.formatter -> t -> unit
Sourceval show : t -> string
Sourcetype constant = Name.constant

See RawData.Constants to allocate global constants

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

Handy constructors to build goals

Sourceval mkPi : loc:Loc.t -> hdloc:Loc.t -> Name.t -> nloc:Loc.t -> ?ty:Type.t -> t -> t
Sourceval mkConj : loc:Loc.t -> hdloc:Loc.t -> t list -> t
Sourceval mkEq : loc:Loc.t -> hdloc:Loc.t -> t -> t -> t
Sourceval 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

Sourceval 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

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

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

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