dedukti

The Dedukti logical framework
IN THIS PACKAGE
Module Typing
val coc : bool ref
type typing_error =
| KindIsNotTypable
| ConvertibilityError of Term.term * Term.typed_context * Term.term * Term.term
| VariableNotFound of Basic.loc * Basic.ident * int * Term.typed_context
| SortExpected of Term.term * Term.typed_context * Term.term
| ProductExpected of Term.term * Term.typed_context * Term.term
| InexpectedKind of Term.term * Term.typed_context
| DomainFreeLambda of Basic.loc
| CannotInferTypeOfPattern of Rule.pattern * Term.typed_context
| CannotSolveConstraints of Rule.untyped_rule * (int * Term.term * Term.term) list
| BracketError1 of Term.term * Term.typed_context
| BracketError2 of Term.term * Term.typed_context * Term.term
| FreeVariableDependsOnBoundVariable of Basic.loc * Basic.ident * int * Term.typed_context * Term.term
| NotImplementedFeature of Basic.loc
| Unconvertible of Basic.loc * Term.term * Term.term
| Convertible of Basic.loc * Term.term * Term.term
| Inhabit of Basic.loc * Term.term * Term.term
exception TypingError of typing_error
type typ = Term.term
val check : Signature.t -> Term.typed_context -> Term.term -> typ -> unit
val checking : Signature.t -> Term.term -> Term.term -> unit
val inference : Signature.t -> Term.term -> typ