Proof assistant for the λΠ-calculus modulo rewriting
Library lambdapi.handle
Module Handle . Tactic
val log_tact : 'a Lplib.Base.outfmt -> 'a
val admitted : int ref

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.

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.

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.

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

val handle : Common.Pos.popt -> bool -> tac_output -> Parsing.Syntax.p_tactic -> int -> tac_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.