Maude-help mailing list

[Keith Ó Dúlaigh <keithod AT cs.nuim.ie>]

Hi,

I'm trying to include a parameterised module within a parameterised 
module like this:

(fmod MAP-UTILS { Z :: TRIV , P :: TRIV } is
   inc MAP{Z, P} .

   var M : Map{Z, P} .
   var I : Z$Elt .
   var J : P$Elt .

   op length : Map {Z, P} -> Nat .
   eq length(empty) = 0 .
   eq length((I |-> J)) = 1 .
   eq length((I |-> J, M)) = s(length(M)) .
   eq length(M) = 0 [owise] .
endfm)

which gives this error message in Maude 2.6 with Full Maude 2.5b:

Warning:(length(empty))=(0)
Error: no parse for eq length(empty) ~ 0
Warning:(length(empty))=(0)
Error: no parse for eq length(empty) ~ 0
Introduced module MAP-UTILS

Any comments on what is wrong with this would be appreciated.

Thanks,
Keith