package dedukti

  1. Overview
  2. Docs
type pattern =
  1. | Var of Basic.loc * Basic.ident * int * pattern list
  2. | Pattern of Basic.loc * Basic.name * pattern list
  3. | Lambda of Basic.loc * Basic.ident * pattern
  4. | Brackets of Term.term
val get_loc_pat : pattern -> Basic.loc
val pattern_to_term : pattern -> Term.term
type wf_pattern =
  1. | LJoker
  2. | LVar of Basic.ident * int * int list
  3. | LLambda of Basic.ident * wf_pattern
  4. | LPattern of Basic.name * wf_pattern array
  5. | LBoundVar of Basic.ident * int * wf_pattern array
val allow_non_linear : bool Stdlib.ref
type constr =
  1. | Linearity of int * int
  2. | Bracket of int * Term.term
type rule_name =
  1. | Delta of Basic.name
  2. | Gamma of bool * Basic.name
type !'a rule = {
  1. name : rule_name;
  2. ctx : 'a;
  3. pat : pattern;
  4. rhs : Term.term;
}
type untyped_rule = Term.untyped_context rule
type typed_rule = Term.typed_context rule
type rule_error =
  1. | BoundVariableExpected of pattern
  2. | DistinctBoundVariablesExpected of Basic.loc * Basic.ident
  3. | VariableBoundOutsideTheGuard of Term.term
  4. | UnboundVariable of Basic.loc * Basic.ident * pattern
  5. | AVariableIsNotAPattern of Basic.loc * Basic.ident
  6. | NonLinearRule of untyped_rule
  7. | NotEnoughArguments of Basic.loc * Basic.ident * int * int * int
  8. | NonLinearNonEqArguments of Basic.loc * Basic.ident
type rule_infos = {
  1. l : Basic.loc;
  2. name : rule_name;
  3. cst : Basic.name;
  4. args : pattern list;
  5. rhs : Term.term;
  6. esize : int;
  7. pats : wf_pattern array;
  8. 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