package dedukti

You can search for identifiers within the package.

in-package search v0.2.0

An implementation of The Lambda-Pi Modulo Theory

Install

sha512=97171b48dd96043d84587581d72edb442f63e7b5ac1695771aa1c3c9074739e15bc7d17678fedb7062acbf403a0bf323d97485c31b92376b80c63b5c2300ee3c

sha256=5e1b6a859dfa1eb2098947a99c7d11ee450f750d96da1720f4834e1505d1096c

Type checking/inference

Sourceval d_typeChecking : Basic.Debug.flag

Sourceval d_rule : Basic.Debug.flag

Sourceval coc : bool ref

Sourceval fail_on_unsatisfiable_constraints : bool ref

Sourcetype 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

Sourceexception Typing_error of typing_error

Sourcetype typ = Term.term

Sourcemodule type S = sig ... end

Sourcemodule Make (R : Reduction.S) : S

Sourcemodule Default : S