package dedukti

  1. Overview
  2. Docs
type red_strategy =
  1. | Hnf
  2. | Snf
  3. | Whnf
type red_cfg = {
  1. select : (Rule.rule_name -> bool) option;
  2. nb_steps : int option;
  3. strategy : red_strategy;
  4. beta : bool;
}
val pp_red_cfg : red_cfg Basic.printer
val default_cfg : red_cfg
val reduction : red_cfg -> Signature.t -> Term.term -> Term.term
val are_convertible : Signature.t -> Term.term -> Term.term -> bool