package dedukti

  1. Overview
  2. Docs
type is_opaque = bool
type is_assertion = bool
type should_fail = bool
type test =
  1. | Convert of Kernel.Term.term * Kernel.Term.term
    (*

    Convertibility between the two given terms.

    *)
  2. | HasType of Kernel.Term.term * Kernel.Term.term
    (*

    Typability test, given a term and a type.

    *)

Possible tests in source files.

exception Assert_error of Kernel.Basic.loc
type entry =
  1. | Decl of Kernel.Basic.loc * Kernel.Basic.ident * Kernel.Signature.scope * Kernel.Signature.staticity * Kernel.Term.term
    (*

    Symbol declaration.

    *)
  2. | Def of Kernel.Basic.loc * Kernel.Basic.ident * Kernel.Signature.scope * is_opaque * Kernel.Term.term option * Kernel.Term.term
    (*

    Definition (possibly opaque).

    *)
  3. | Rules of Kernel.Basic.loc * Kernel.Rule.partially_typed_rule list
    (*

    Reduction rules declaration.

    *)
  4. | Eval of Kernel.Basic.loc * Kernel.Reduction.red_cfg * Kernel.Term.term
    (*

    Evaluation command.

    *)
  5. | Check of Kernel.Basic.loc * is_assertion * should_fail * test
    (*

    Test command.

    *)
  6. | Infer of Kernel.Basic.loc * Kernel.Reduction.red_cfg * Kernel.Term.term
    (*

    Type inference command.

    *)
  7. | Print of Kernel.Basic.loc * string
    (*

    Printing command.

    *)
  8. | DTree of Kernel.Basic.loc * Kernel.Basic.mident option * Kernel.Basic.ident
    (*

    Decision tree printing.

    *)
  9. | Name of Kernel.Basic.loc * Kernel.Basic.mident
    (*
    • deprecated

      Ignored #NAME command. Module name defaults to the file name without extension.

    *)
  10. | Require of Kernel.Basic.loc * Kernel.Basic.mident
    (*

    Require command.

    *)

Single source file entry.

val loc_of_entry : entry -> Kernel.Basic.loc
val pp_entry : entry Kernel.Basic.printer