package dedukti

You can search for identifiers within the package.

in-package search v0.2.0

Legend:
Library
Module
Module type
Parameter
Class
Class type

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 infer : Signature.t -> Term.typed_context -> Term.term -> typ

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

val check_rule : Signature.t -> Rule.untyped_rule -> Rule.typed_rule