-- FILE: nat+.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) .
}

eof

set verbose on

select NAT+
red s 0 + 0 .
parse s 0 + 0 .
describe op (s _)
describe op (_ + _)

open (NAT+ + EQL)

red s 0 + 0 .
parse s 0 + 0 .
describe op (s _)
describe op (_ + _)

op n : -> Nat .
red 0 + n = n .

sh ops
sh op (s _)
sh op (_ + _)

close