package lambdapi
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=2c251021b6fac40c05282ca183902da5b1008e69d9179d7a9543905c2c21a28a
sha512=69535f92766e6fedc2675fc214f0fb699bde2a06aa91d338c93c99756235a293cf16776f6328973dda07cf2ad402e58fe3104a08f1a896990c1778b42f7f9fcf
doc/lambdapi.handle/Handle/Proof/index.html
Module Handle.Proof
Source
Proofs and tactics.
type goal_typ = {
goal_meta : Core.Term.meta;
(*Goal metavariable.
*)goal_hyps : Core.Env.t;
(*Precomputed scoping environment.
*)goal_type : Core.Term.term;
(*Precomputed type.
*)
}
Type of goals.
add_goals_of_problem p gs
extends the list of goals gs
with the metavariables and constraints of p
.
type proof_state = {
proof_name : Common.Pos.strloc;
(*Name of the theorem.
*)proof_term : Core.Term.meta option;
(*Optional metavariable holding the goal associated to a symbol used as a theorem/definition and not just a simple declaration
*)proof_goals : goal list;
(*Open goals (focused goal is first).
*)
}
Representation of the proof state of a theorem.
finished ps
tells whether there are unsolved goals in ps
.
goals ppf gl
prints the goal list gl
to channel ppf
.
remove_solved_goals ps
removes from the proof state ps
the typing goals that are solved.
meta_of_key ps i
returns Some m
where m
is a meta of ps
whose key is i
, or else it returns None
.
focus_env ps
returns the scoping environment of the focused goal or the empty environment if there is none.