package lambdapi
-
lambdapi.tool
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package lambdapi
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
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.
val is_typ : goal -> boolval is_unif : goal -> boolval get_constr : goal -> Core.Term.constrmodule Goal : sig ... endval add_goals_of_problem : Core.Term.problem -> goal list -> goal listadd_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 -> boolfinished ps tells whether there are unsolved goals in ps.
val goals : proof_state Lplib.Base.ppgoals ppf gl prints the goal list gl to channel ppf.
val remove_solved_goals : proof_state -> proof_stateremove_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 optionmeta_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.tfocus_env ps returns the scoping environment of the focused goal or the empty environment if there is none.