package lambdapi

  1. Overview
  2. Docs

Handling of tactics.

val log : 'a Lplib.Base.outfmt -> 'a
val 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.

val admitted : int Stdlib.ref
val 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.

val admit_meta : Core.Sig_state.t -> Common.Pos.popt -> Core.Term.meta -> unit

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.

type tac_output = Proof.proof_state * Query.result

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.