lambdapi
Proof assistant for the λΠ-calculus modulo rewriting
1024" x-on:close-sidebar="sidebar=window.innerWidth > 1024 && true">
package lambdapi
-
lambdapi.tool
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
val infer_noexn :
Term.problem ->
Term.ctxt ->
Term.term ->
(Term.term * Term.term) option
infer_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 option
check_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
ON THIS PAGE
No table of contents