-
lambdapi.tool
Library
Module
Module type
Parameter
Class
Class type
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.
val is_typ : goal -> bool
val is_unif : goal -> bool
val get_constr : goal -> Core.Term.constr
module Goal : sig ... end
val add_goals_of_problem : Core.Term.problem -> goal list -> goal list
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.
val finished : proof_state -> bool
finished ps
tells whether there are unsolved goals in ps
.
val goals : proof_state Lplib.Base.pp
goals ppf gl
prints the goal list gl
to channel ppf
.
val remove_solved_goals : proof_state -> proof_state
remove_solved_goals ps
removes from the proof state ps
the typing goals that are solved.
val meta_of_key : proof_state -> int -> Core.Term.meta option
meta_of_key ps i
returns Some m
where m
is a meta of ps
whose key is i
, or else it returns None
.
val focus_env : proof_state option -> Core.Env.t
focus_env ps
returns the scoping environment of the focused goal or the empty environment if there is none.