package lambdapi
Install
dune-project
Dependency
Authors
Maintainers
Sources
sha256=66d7d29f7a0d10493b8178c4c3aeb247971e24fab3eba1c54887e1b9a82fe005
sha512=69ecf2406e4c7225ab7f8ebe11624db5d2ab989c8f30f5b6e5d426fd8ef9102f142a2840af16fb9103bb712ebcf7d314635f8b413a05df66e7b7a38548867032
doc/lambdapi.handle/Handle/Proof/index.html
Module Handle.ProofSource
Proofs and tactics.
type goal_typ = {goal_meta : Core.Term.meta;goal_hyps : Core.Env.t;goal_type : Core.Term.term;
}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.
pp_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.
meta_of_name ps n returns Some m where m is a meta of ps whose name is n, or else it returns None.
focus_env ps returns the scoping environment of the focused goal or the empty environment if there is none.