package elpi

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

Install 

dune-project
 Dependency

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

Authors

  1. C
    Claudio Sacerdoti Coen
  2. E
    Enrico Tassi

Maintainers

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

Sources

elpi-3.7.3.tbz
sha256=6c68078b96d4c179734d829b25aad06c36e7fabd1c6385d2d6c0074a5112f7b9
sha512=761415b8a54ae8ebea0f387e531c4872116cac8406e467e2cde959821c497849558990870d88de673a5890e43cc712d475a1afcbdef0c2303e1d8210927aa967

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;
}
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