-- FILE: nat+err.mod

mod! NAT+ {
  [Zero NzNat < Nat]
  op 0 : -> Zero
  op s_ : Nat -> NzNat
  op _+_ : Nat Nat -> Nat
  
  vars M N : Nat
  eq    0  + N = N .
  eq (s M) + N = s(M,N) .
}

open NAT+

parse s(M,N) .
parse M .
parse N .

close

mod! NAT+DEBUG {
  [Zero NzNat < Nat]
  op 0 : -> Zero
  op s_ : Nat -> NzNat
  op _+_ : Nat Nat -> Nat
  
  vars M N : Nat
  eq    0  + N = N .
}

select NAT+DEBUG

parse s(M,N) .
parse M .
parse N .
parse s(M + N) .