dedukti

The Dedukti logical framework
IN THIS PACKAGE
Module Reduction
type red_strategy =
| Hnf
| Snf
| Whnf
type red_cfg = {
select : ( Rule.rule_name -> bool ) option;
nb_steps : int option;
strategy : red_strategy;
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