-- Int0 where nz requires a proof that its Int isn't 0.

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

open Int0

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

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

-- Int0.nz 8 _
#eval add ((nz 5) (by decide)) ((nz 3) (by decide))
-- Int0.z
#eval add ((nz 5) (by decide)) ((nz (-5)) (by decide))
-- error: 0 ≠ 0 is false
-- #eval nz 0

-- div is still partial: n2 can still be z.
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))
--  | nz a _, nz b _ => .ok (nz (a / b))

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