Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
type t = goal
val ctxt : goal -> Core.Term.ctxt
ctxt g
returns the typing context of the goal g
.
val env : goal -> Core.Env.t
env g
returns the scoping environment of the goal g
.
val of_meta : Core.Term.meta -> goal
of_meta m
creates a goal from the meta m
.
val simpl : (Core.Term.term -> Core.Term.term) -> goal -> goal
simpl f g
simplifies the goal g
with the function f
.
val bindlib_ctxt : goal -> Bindlib.ctxt
bindlib_ctxt g
computes a Bindlib context from a goal.
val pp : goal Lplib.Base.pp
pp ppf g
prints on ppf
the goal g
without its hypotheses.
val hyps : goal Lplib.Base.pp
hyps ppf g
prints on ppf
the hypotheses of the goal g
.