dedukti

The Dedukti logical framework
IN THIS PACKAGE
Module Entry
type is_opaque = bool
type is_assertion = bool
type should_fail = bool
type test =
| Convert of Term.term * Term.term
| HasType of Term.term * Term.term
type entry =
| Decl of Basic.loc * Basic.ident * Signature.staticity * Term.term
| Def of Basic.loc * Basic.ident * is_opaque * Term.term option * Term.term
| Rules of Rule.untyped_rule list
| Eval of Basic.loc * Reduction.red_cfg * Term.term
| Check of Basic.loc * is_assertion * should_fail * test
| Infer of Basic.loc * Reduction.red_cfg * Term.term
| Print of Basic.loc * string
| DTree of Basic.loc * Basic.mident option * Basic.ident
| Name of Basic.loc * Basic.mident
| Require of Basic.loc * Basic.mident
val pp_entry : entry Basic.printer