package dedukti

  1. Overview
  2. Docs
val coc : bool Stdlib.ref
type typing_error =
  1. | KindIsNotTypable
  2. | ConvertibilityError of Term.term * Term.typed_context * Term.term * Term.term
  3. | VariableNotFound of Basic.loc * Basic.ident * int * Term.typed_context
  4. | SortExpected of Term.term * Term.typed_context * Term.term
  5. | ProductExpected of Term.term * Term.typed_context * Term.term
  6. | InexpectedKind of Term.term * Term.typed_context
  7. | DomainFreeLambda of Basic.loc
  8. | CannotInferTypeOfPattern of Rule.pattern * Term.typed_context
  9. | CannotSolveConstraints of Rule.untyped_rule * (int * Term.term * Term.term) list
  10. | BracketError1 of Term.term * Term.typed_context
  11. | BracketError2 of Term.term * Term.typed_context * Term.term
  12. | FreeVariableDependsOnBoundVariable of Basic.loc * Basic.ident * int * Term.typed_context * Term.term
  13. | NotImplementedFeature of Basic.loc
  14. | Unconvertible of Basic.loc * Term.term * Term.term
  15. | Convertible of Basic.loc * Term.term * Term.term
  16. | 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