package lambdapi
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=2c251021b6fac40c05282ca183902da5b1008e69d9179d7a9543905c2c21a28a
sha512=69535f92766e6fedc2675fc214f0fb699bde2a06aa91d338c93c99756235a293cf16776f6328973dda07cf2ad402e58fe3104a08f1a896990c1778b42f7f9fcf
doc/lambdapi.handle/Handle/Tactic/index.html
Module Handle.Tactic
Source
Handling of tactics.
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
.
val tac_admit :
Core.Sig_state.t ->
Common.Pos.popt ->
Proof.proof_state ->
Proof.goal_typ ->
Proof.proof_state
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.
val tac_refine :
?check:bool ->
Common.Pos.popt ->
Proof.proof_state ->
Proof.goal_typ ->
Proof.goal list ->
Core.Term.problem ->
Core.Term.term ->
Proof.proof_state
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.
val tac_induction :
Common.Pos.popt ->
Proof.proof_state ->
Proof.goal_typ ->
Proof.goal list ->
Proof.proof_state
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
.
Representation of a tactic output.
val handle :
Core.Sig_state.t ->
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.