package dedukti

You can search for identifiers within the package.

in-package search v0.2.0

package dedukti

dedukti.kernel
- Basic
  - LList
- Confluence
- Dtree
- Entry
- Env
- Errors
- Matching
- Pp
- Reduction
- Rule
- Signature
- Subst
  - Subst
- Term
- Typing
- Version
dedukti.parser
- Parser

Legend:
Library
Module
Module type
Parameter
Class
Class type

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