package dedukti

You can search for identifiers within the package.

in-package search v0.2.0

package dedukti

dedukti.kernel
- Basic
  - LList
- Confluence
- Dtree
- Entry
- Env
- Errors
- Matching
- Pp
- Reduction
- Rule
- Signature
- Subst
  - Subst
- Term
- Typing
- Version
dedukti.parser
- Parser

Legend:
Library
Module
Module type
Parameter
Class
Class type

type pattern =

| Var of Basic.loc * Basic.ident * int * pattern list
| Pattern of Basic.loc * Basic.name * pattern list
| Lambda of Basic.loc * Basic.ident * pattern
| Brackets of Term.term

val get_loc_pat : pattern -> Basic.loc

val pattern_to_term : pattern -> Term.term

type wf_pattern =

| LJoker
| LVar of Basic.ident * int * int list
| LLambda of Basic.ident * wf_pattern
| LPattern of Basic.name * wf_pattern array
| LBoundVar of Basic.ident * int * wf_pattern array

val allow_non_linear : bool ref

type constr =

| Linearity of int * int
| Bracket of int * Term.term

type rule_name =

| Delta of Basic.name
| Gamma of bool * Basic.name

type !'a rule = {

name : rule_name;
ctx : 'a;
pat : pattern;
rhs : Term.term;

}

type untyped_rule = Term.untyped_context rule

type typed_rule = Term.typed_context rule

type rule_error =

| BoundVariableExpected of pattern
| DistinctBoundVariablesExpected of Basic.loc * Basic.ident
| VariableBoundOutsideTheGuard of Term.term
| UnboundVariable of Basic.loc * Basic.ident * pattern
| AVariableIsNotAPattern of Basic.loc * Basic.ident
| NonLinearRule of untyped_rule
| NotEnoughArguments of Basic.loc * Basic.ident * int * int * int
| NonLinearNonEqArguments of Basic.loc * Basic.ident

type rule_infos = {

l : Basic.loc;
name : rule_name;
cst : Basic.name;
args : pattern list;
rhs : Term.term;
esize : int;
pats : wf_pattern array;
constraints : constr list;

}

val pattern_of_rule_infos : rule_infos -> pattern

val to_rule_infos : untyped_rule -> (rule_infos, rule_error) Basic.error

val pp_rule_name : rule_name Basic.printer

val pp_untyped_rule : untyped_rule Basic.printer

val pp_typed_rule : typed_rule Basic.printer

val pp_pattern : pattern Basic.printer

val pp_wf_pattern : wf_pattern Basic.printer

val pp_untyped_context : Term.untyped_context Basic.printer

val pp_typed_context : Term.typed_context Basic.printer

val pp_rule_infos : rule_infos Basic.printer