package lambdapi

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

Install

Dune Dependency

Authors

Maintainers

Sources

lambdapi-2.4.1.tbz
sha256=221dff97ab245c49b7e6480fa2a3a331ab70eb86dd5d521e2c73151029bbb787
sha512=a39961bb7f04f739660a98a52981d4793709619cd21310ca6982ba78af81ef09e01c7517ee3b8b2687b09f7d2614d878c1d69494ca6ab8ef8205d240c216ce8a

doc/lambdapi.handle/Handle/Tactic/index.html

Module Handle.TacticSource

Handling of tactics.

Sourceval log : 'a Lplib.Base.outfmt -> 'a
Sourceval admitted_initial_value : int

Number of admitted axioms in the current signature. Used to name the generated axioms. This reference is reset in Compile for each new compiled module.

Sourceval admitted : int ref
Sourceval reset_admitted : unit -> unit

add_axiom ss sym_pos m adds in signature state ss a new axiom symbol of type !(m.meta_type) and instantiate m with it. WARNING: It does not check whether the type of m contains metavariables. Return updated signature state ss and the new axiom symbol.

admit_meta ss sym_pos m adds as many axioms as needed in the signature state ss to instantiate the metavariable m by a fresh axiom added to the signature ss.

tac_admit ss pos ps gt admits typing goal gt.

tac_solve pos ps tries to simplify the unification goals of the proof state ps and fails if constraints are unsolvable.

tac_refine pos ps gt gs p t refines the typing goal gt with t. p is the set of metavariables created by the scoping of t.

ind_data t returns the ind_data structure of s if t is of the form s t1 .. tn with s an inductive type. Fails otherwise.

tac_induction pos ps gt tries to apply the induction tactic on the typing goal gt.

Sourceval count_products : Core.Term.ctxt -> Core.Term.term -> int

count_products a returns the number of consecutive products at the top of the term a.

Representation of a tactic output.

handle sym_pos prv r tac n applies the tactic tac from the previous tactic output r and checks that the number of goals of the new proof state is compatible with the number n of subproofs.

OCaml

Innovation. Community. Security.