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

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

get_prod_ids env do_whnf t returns the list v1;..;vn if do_whnf is true and whnf t is of the form Π v1:A1, .., Π vn:An, u with u not a product, or if do_whnf is false and t is of the form Π v1:A1, .., Π vn:An, u with u not a product.

Builtin tactic names.

get_config ss pos build the configuration using ss.

p_term pos t converts the term t into a p_term at position pos.

p_tactic t interprets the term t as a tactic.

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.