Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package dedukti
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
val infer : Signature.t -> Term.typed_context -> Term.term -> typinfer sg ctx te infers a type for the term te in the signature sg and context ctx The context is assumed to be well-formed
val check : Signature.t -> Term.typed_context -> Term.term -> typ -> unitcheck sg ctx te ty checks that the term te has type ty in the signature sg and context ty.ctx. ty is assumed to be well-typed in ctx and ctx is assumed to be well-formed
val checking : Signature.t -> Term.term -> Term.term -> unitchecking sg te ty checks that te has type ty in the empty context. ty is typechecked first.
val inference : Signature.t -> Term.term -> typinference sg ctx te infers a type for the term te in empty context.
val check_rule :
Signature.t ->
Rule.partially_typed_rule ->
Exsubst.ExSubst.t * Rule.typed_rulecheck_rule sg ru checks that a rule is well-typed.