package lambdapi
Legend:
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.

type goal =
| Typ of goal_typ(*

Typing goal.

*)
| Unif of Core.Term.constr(*

Unification goal.

*)
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.

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.