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
Type inference and checking
val infer_noexn :
Term.problem ->
Term.ctxt ->
Term.term ->
(Term.term * Term.term) optioninfer_noexn p ctx t returns None if the type of t in context ctx cannot be inferred, or Some a where a is some type of t in the context ctx, possibly adding new constraints in p. The metavariables of p are updated when a metavariable is instantiated or created. ctx must be well sorted.
val check_noexn :
Term.problem ->
Term.ctxt ->
Term.term ->
Term.term ->
Term.term optioncheck_noexn p ctx t a tells whether the term t has type a in the context ctx, possibly adding new constraints in p. The metavariables of p are updated when a metavariable is instantiated or created. The context ctx and the type a must be well sorted.
val check_sort_noexn :
Term.problem ->
Term.ctxt ->
Term.term ->
(Term.term * Term.term) option