package dedukti

  1. Overview
  2. Docs
type signature_error =
  1. | UnmarshalBadVersionNumber of Basic.loc * string
  2. | UnmarshalSysError of Basic.loc * string * string
  3. | UnmarshalUnknown of Basic.loc * string
  4. | SymbolNotFound of Basic.loc * Basic.name
  5. | AlreadyDefinedSymbol of Basic.loc * Basic.ident
  6. | CannotMakeRuleInfos of Rule.rule_error
  7. | CannotBuildDtree of Dtree.dtree_error
  8. | CannotAddRewriteRules of Basic.loc * Basic.ident
  9. | ConfluenceErrorImport of Basic.loc * Basic.mident * Confluence.confluence_error
  10. | ConfluenceErrorRules of Basic.loc * Rule.rule_infos list * Confluence.confluence_error
  11. | GuardNotSatisfied of Basic.loc * Term.term * Term.term
exception SignatureError of signature_error
type staticity =
  1. | Static
  2. | 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