Maude-help mailing list

[Marc Boyer <Marc.Boyer AT enseeiht.fr>]

Dear all,

how can I exclude the built-in symblos from traces ?
Here is a minimal example:

--------------- testExclude.maude ------------------
fmod TEST-EXCLUDE is
  protecting NAT .
  sort S .
  op f _ : Nat -> S [ctor] .
  op _ + _ : S S -> S [comm] .
  vars n n' : Nat .
  eq (f n) + (f n') = f (n + n' ) .
endfm
set trace on .
trace exclude NAT .
red (f 1) + (f 2) .
---------------------------------------------------

And here is the output

==========================================
reduce in TEST-EXCLUDE : f 1 + f 2 .
*********** equation
eq f n + f n' = f (n + n') .
n --> 1
n' --> 2
f 1 + f 2
--->
f (1 + 2)
*********** equation
(built-in equation for symbol _+_)
1 + 2
--->
3
rewrites: 2 in 0ms cpu (0ms real) (~ rewrites/second)
result S: f 3

I would like to hide the 1 + 2 ---> 3 rewrite.


--
Marc Boyer                  INPT - ENSEEIHT - Dép. Télécoms & Réseaux
Tel: (33)  5.61.58.80.21                                     IRIT-IRT
Fax: (33)  5.61.58.80.14                              2, rue Camichel
http://www.enseeiht.fr/~boyer/                 31071 TOULOUSE Cedex 7