package elpi

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

Install

dune-project
 Dependency

Authors

Maintainers

Sources

elpi-3.4.0.tbz
sha256=9955d95d69b1ffb6770daad42f2b15d44a8888843817dff272d44ef8a3480b5a
sha512=408bfb46efeba45d0c5e36e8478d9e9b2f01f38de88c10621deeedc69e4c2b007d859fec520ef5652ab33bf00106edbda421f16503eeff397ceb57a61e01fce2

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

Module ScopedTerm.SimpleTermSource

Sourcetype 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_ =
  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
Sourceand t = {
  1. it : t_;
  2. loc : Elpi_util.Util.Loc.t;
}
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 mkImplication : loc:Elpi_util.Util.Loc.t -> hdloc:Elpi_util.Util.Loc.t -> t -> 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:Elpi_util.Util.Loc.t -> 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