package dedukti

  1. Overview
  2. Docs
An implementation of The Lambda-Pi Modulo Theory

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (2)

Authors

  1. D
    dedukti-dev@inria.fr

Maintainers

  1. D
    dedukti-dev@inria.fr

Sources

v2.7.tar.gz
sha512=97171b48dd96043d84587581d72edb442f63e7b5ac1695771aa1c3c9074739e15bc7d17678fedb7062acbf403a0bf323d97485c31b92376b80c63b5c2300ee3c
sha256=5e1b6a859dfa1eb2098947a99c7d11ee450f750d96da1720f4834e1505d1096c

doc/dedukti.parsers/Parsers/Entry/index.html

Module Parsers.EntrySource

Sourcetype is_opaque = bool
Sourcetype is_assertion = bool
Sourcetype should_fail = bool
Sourcetype 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.

Sourceexception Assert_error of Kernel.Basic.loc
Sourcetype 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.

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