package elpi

  1. Overview
  2. Docs
package elpi
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t_ =
  1. | Impl of bool * t * t
  2. | Const of Scope.t * Name.t
  3. | Discard
  4. | Var of Name.t * t list
    (*

    unification variable

    *)
  5. | App of Scope.t * Name.t * t * t list
  6. | Lam of (Name.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 -> constant -> t -> t list -> t
val mkAppBound : loc:Loc.t -> language:Scope.language -> Name.t -> t -> t list -> t
val mkVar : loc: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 * Scope.language) option -> ?ty:Type.t -> t -> t
val mkDiscard : loc:Loc.t -> t
val mkImplication : loc:Loc.t -> t -> t -> t

Handy constructors to build goals

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

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct