diff options
Diffstat (limited to 'test/KB/terms.mli')
| -rw-r--r-- | test/KB/terms.mli | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/test/KB/terms.mli b/test/KB/terms.mli new file mode 100644 index 0000000000..3e3f831b36 --- /dev/null +++ b/test/KB/terms.mli @@ -0,0 +1,17 @@ +type term = + Var of int + | Term of string * term list + +val union: 'a list -> 'a list -> 'a list +val vars: term -> int list +val vars_of_list: term list -> int list +val substitute: (int * term) list -> term -> term +val replace: term -> int list -> term -> term +val replace_nth: int -> term list -> int list -> term -> term list +val matching: term -> term -> (int * term) list +val compsubst: (int * term) list -> (int * term) list -> (int * term) list +val occurs: int -> term -> bool +val unify: term -> term -> (int * term) list +val infixes: string list +val pretty_term: term -> unit +val pretty_close: term -> unit |