dedukti

The Dedukti logical framework
IN THIS PACKAGE
Module Signature
type signature_error =
| UnmarshalBadVersionNumber of Basic.loc * string
| UnmarshalSysError of Basic.loc * string * string
| UnmarshalUnknown of Basic.loc * string
| SymbolNotFound of Basic.loc * Basic.name
| AlreadyDefinedSymbol of Basic.loc * Basic.ident
| CannotMakeRuleInfos of Rule.rule_error
| CannotBuildDtree of Dtree.dtree_error
| CannotAddRewriteRules of Basic.loc * Basic.ident
| ConfluenceErrorImport of Basic.loc * Basic.mident * Confluence.confluence_error
| ConfluenceErrorRules of Basic.loc * Rule.rule_infos list * Confluence.confluence_error
| GuardNotSatisfied of Basic.loc * Term.term * Term.term
exception SignatureError of signature_error
type staticity =
| Static
| Definable
type t
val make : string -> t
val get_name : t -> Basic.mident
val export : t -> bool
val import : t -> Basic.loc -> Basic.mident -> unit
val is_injective : t -> Basic.loc -> Basic.name -> bool
val get_type : t -> Basic.loc -> Basic.name -> Term.term
val get_dtree : t -> ( Rule.rule_name -> bool ) option -> Basic.loc -> Basic.name -> (int * Dtree.dtree) option
val add_declaration : t -> Basic.loc -> Basic.ident -> staticity -> Term.term -> unit
val add_rules : t -> Rule.untyped_rule list -> unit