package dedukti

You can search for identifiers within the package.

in-package search v0.2.0

Legend:
Library
Module
Module type
Parameter
Class
Class type

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 =

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