Maude-help mailing list

[Guilherme Horta Alvares Da Silva <alvares AT chalmers.se>]

I want to debug my Maude program and I want it to show in every equation why it does not pattern match.

For example:

```

fmod EX is

  sort Nat .

  op z : -> Nat [ctor] .

  op s_ : Nat -> Nat [ctor iter] .

  op f : Nat -> Nat .

  var x : Nat .

  eq f(z) = z .

endfm

set break on .

break select f .

debug red f(s z) .

```

I would like it to break in the equation f(z), and just says that s z does not match z.

This example is trivial, but I need this feature for more complex examples. I usually have to manually do a lot of match commands.

Thank you for reading this question. I didn't find anything the solution in the documentation.