package elpi

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

Install 

dune-project
 Dependency

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

Authors

  1. C
    Claudio Sacerdoti Coen
  2. E
    Enrico Tassi

Maintainers

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

Sources

elpi-3.4.1.tbz
sha256=deb40fc3dd5d1c0aa9eb52931e4d54384aa1e6cc96ad9675575ff5784f1cc88f
sha512=71092d086b9ad72a5b6e08ecfa2fa896bd109730c1896ff0cfe7465be6d7dc5faff033e0bd518e450279925e38ac1cb254ce18f90235b3492508ce346a3d1efc

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