-- Int0 as in Shplait: z, or nz of any Int. Nothing stops nz 0.

inductive Int0 where
  | nz (n : Int)
  | z
  deriving Repr

open Int0

def i (n : Int) : Int0 := if n == 0 then z else nz n

def add : Int0 → Int0 → Int0
  | z,    z    => z
  | z,    nz b => nz b
  | nz a, z    => nz a
  | nz a, nz b => i (a + b)
--  | nz a, nz b => nz (a + b)

-- Int0.nz 8
#eval add (nz 5) (nz 3)
-- Int0.z or Int0.nz 0
#eval add (nz 5) (nz (-5))
-- Int0.nz 0: accepted
#eval nz 0

def dynDiv (n1 n2 : Int0) : Except String Int0 :=
  match n1, n2 with
  | z,    z    => .error "undefined"
  | z,    nz _ => .ok z
  | nz _, z    => .error "divide by zero"
  | nz a, nz b => .ok (i (a / b))

-- Except.ok (Int0.nz 5)
#eval dynDiv (nz 10) (nz 2)
-- Except.ok (Int0.z)
#eval dynDiv (nz 1) (nz 2)
-- Except.error "divide by zero"
#eval dynDiv (nz 10) z

-- As in Shplait, nz is a constructor, not a type:
-- def div (n1 : Int0) (n2 : nz) : Int0 := n1   -- error: type expected