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

Type checking/inference

val d_typeChecking : Basic.Debug.flag

val d_rule : Basic.Debug.flag

val coc : bool ref

val fail_on_unsatisfiable_constraints : bool ref

type typing_error =

| KindIsNotTypable
| ConvertibilityError of Term.term * Term.typed_context * Term.term * Term.term
| AnnotConvertibilityError of Basic.loc * Basic.ident * 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
| UnsatisfiableConstraints of Rule.partially_typed_rule * int * Term.term * Term.term
| BracketExprBoundVar of Term.term * Term.typed_context
| BracketExpectedTypeBoundVar of Term.term * Term.typed_context * Term.term
| BracketExpectedTypeRightVar of Term.term * Term.typed_context * Term.term
| TypingCircularity of Basic.loc * Basic.ident * int * 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 Typing_error of typing_error

type typ = Term.term

module type S = sig ... end

module Make (R : Reduction.S) : S

module Default : S