package elpi

  1. Overview
  2. Docs
ELPI - Embeddable λProlog Interpreter

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (25)

Authors

  1. C
    Claudio Sacerdoti Coen
  2. E
    Enrico Tassi

Maintainers

  1. E
    Enrico Tassi <enrico.tassi@inria.fr>

Sources

elpi-3.7.1.tbz
sha256=0109f44fd6c08f5eed01c559765dcf4e3e2b8b47c25d026f0153757459f5f466
sha512=62fb7bce9d8d0505458b9686a9ab112f4f988ab6e2051bb623d53308f175abd72ed74c8962e5469380ec989b80c58a77b31c8bbfb7e8b2b60953b11b436f6647

doc/elpi.compiler/Elpi_compiler/Compiler_data/ScopedTerm/QTerm/index.html

Module ScopedTerm.QTermSource

include module type of struct include SimpleTerm end
Sourcetype impl_kind = SimpleTerm.impl_kind =
  1. | L2R
  2. | L2RBang
  3. | R2L
Sourceval is_implf : Elpi_parser.Ast.Func.t -> bool
Sourceval func_to_impl_kind : Elpi_parser.Ast.Func.t -> impl_kind
Sourcetype t_ = SimpleTerm.t_ =
  1. | Impl of impl_kind * Elpi_util.Util.Loc.t * t * t
  2. | Const of Scope.t * F.t
  3. | Discard
  4. | Var of F.t * Elpi_util.Util.Loc.t * t list
  5. | App of Scope.t * F.t * Elpi_util.Util.Loc.t * t * t list
  6. | Lam of (F.t * Elpi_util.Util.Loc.t * Scope.language) option * ScopedTypeExpression.SimpleType.t option * t
  7. | Opaque of Elpi_util.Util.CData.t
  8. | Cast of t * ScopedTypeExpression.SimpleType.t
Sourceval pp_t_ : Ppx_deriving_runtime.Format.formatter -> t_ -> Ppx_deriving_runtime.unit
Sourceval show_t_ : t_ -> Ppx_deriving_runtime.string
Sourcetype constant = int
Sourceval mkBound : loc:Elpi_util.Util.Loc.t -> language:Scope.language -> F.t -> t
Sourceval mkAppBound : loc:Elpi_util.Util.Loc.t -> hdloc:Elpi_util.Util.Loc.t -> language:Scope.language -> F.t -> t -> t list -> t
Sourceval mkVar : loc:Elpi_util.Util.Loc.t -> hdloc:Elpi_util.Util.Loc.t -> F.t -> t list -> t
Sourceval mkDiscard : loc:Elpi_util.Util.Loc.t -> t
Sourceval mkLam : loc:Elpi_util.Util.Loc.t -> (F.t * Elpi_util.Util.Loc.t * Scope.language) option -> ?ty:??? -> t -> t
Sourceval mkImplication : loc:Elpi_util.Util.Loc.t -> hdloc:Elpi_util.Util.Loc.t -> t -> t -> t
Sourceval mkPi : loc:Elpi_util.Util.Loc.t -> hdloc:Elpi_util.Util.Loc.t -> F.t -> nloc:Elpi_util.Util.Loc.t -> ?ty:??? -> t -> t
Sourceval mkConj : loc:Elpi_util.Util.Loc.t -> hdloc:Elpi_util.Util.Loc.t -> t list -> t
Sourceval mkEq : loc:Elpi_util.Util.Loc.t -> hdloc:Elpi_util.Util.Loc.t -> t -> t -> t
Sourceval mkNil : loc:Elpi_util.Util.Loc.t -> t
Sourceval mkCons : ?loc:??? -> hdloc:Elpi_util.Util.Loc.t -> t -> t -> t
Sourceval list_to_lp_list : loc:Elpi_util.Util.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 : SimpleTerm.t -> SimpleTerm.t list -> SimpleTerm.t
Sourceval extend_spill_hyp_from_quotation : SimpleTerm.t -> t list -> t
Sourceval is_spill_from_quotation : SimpleTerm.t -> bool