package lambdapi

  1. Overview
  2. Docs
Proof assistant for the λΠ-calculus modulo rewriting

Install

Dune Dependency

Authors

Maintainers

Sources

lambdapi-2.5.1.tbz
sha256=2c251021b6fac40c05282ca183902da5b1008e69d9179d7a9543905c2c21a28a
sha512=69535f92766e6fedc2675fc214f0fb699bde2a06aa91d338c93c99756235a293cf16776f6328973dda07cf2ad402e58fe3104a08f1a896990c1778b42f7f9fcf

doc/lambdapi.export/Export/Xtc/index.html

Module Export.XtcSource

This module provides a function to translate a simply typed signature to the XTC format used in the termination competition.

Remarks:

  • SizeChangeTool accepts an extension of the XTC format with lambda and application in types and:

<arrow> <var>...</var> <type>...</type> <type>...</type> </arrow>

<typeLevelRule> <TLlhs>...</TLlhs> <TLrhs>...</TLrhs> </typeLevelRule>

Sourceval syms : string Core.Term.SymMap.t ref

syms maps every symbol to a name.

bvars is the set of abstracted variables.

Sourceval nb_rules : int ref

nb_rules is the number of rewrite rules.

Sourceval pvars : (int * int * Core.Term.term) list ref

pvars is the list of all pattern variables with their type.

Sourceval type_of_pvar : Core.Term.term array ref

typ is a reference to the types of the pvars of the current rules.

sym_name s translates the symbol name of s.

Sourceval add_sym : Core.Term.sym -> unit

add_sym declares a Lambdapi symbol.

type_sym ppf s translates the Lambdapi type symbol s.

sym ppf s translates the Lambdapi symbol s.

Sourceval add_bvar : Core.Term.tvar -> unit

add_bvar v declares an abstracted Lambdapi variable.

bvar v translates the Lambdapi bound variable v.

Sourceval pvar : int Lplib.Base.pp

pvar i translates the Lambdapi pattern variable i.

term ppf t translates the term t.

Sourceval pvar_app : (int * Core.Term.term array) Lplib.Base.pp
Sourceval add_pvars : Core.Term.sym -> Core.Term.rule -> unit

add_pvars s r adds the types of the pvars of r in pvars.

rule ppf r translates the pair of terms r as a rule.

sym_rule ppf s r increases the number of rules and translates the sym_rule r.

Translate the rules of symbol s.

Sourceval rules_of_sign : Core.Sign.t Lplib.Base.pp

Translate the rules of a dependency except if it is a ghost signature.

sign ppf s translates the Lambdapi signature s.

OCaml

Innovation. Community. Security.