blob: db80f48163ffbc0db5e92371326240ca64aec5ae (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
|
(***********************************************************************)
(* *)
(* OCaml *)
(* *)
(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
(* *)
(* Copyright 1996 Institut National de Recherche en Informatique et *)
(* en Automatique. All rights reserved. This file is distributed *)
(* under the terms of the Q Public License version 1.0. *)
(* *)
(***********************************************************************)
open Terms
type rule =
{ number: int;
numvars: int;
lhs: term;
rhs: term }
val mk_rule: int -> term -> term -> rule
val check_rules: rule list -> int
val pretty_rule: rule -> unit
val pretty_rules: rule list -> unit
val reduce: term -> term -> term -> term
val reducible: term -> term -> bool
val mreduce: rule list -> term -> term
val mrewrite1: rule list -> term -> term
val mrewrite1_sons: rule list -> term list -> term list
val mrewrite_all: rule list -> term -> term
|
