[Agda] Alternative partial function attempt

[Tristan Wibberley]

Hi all,

I've tried this approach instead:

module first where

data ¿⊥ : Set where
record ¿⊤ : Set where

data ℕ : Set where
  zero : ℕ
  succ : ℕ -> ℕ

_+_ : ℕ -> ℕ -> ℕ
_+_ zero b = b
_+_ (succ a) b = a + (succ b)

data _¿≤ℕ_ : ℕ -> ℕ -> Set where
  ¿≤ℕ/z : (m : ℕ) -> zero ¿≤ℕ m
  ¿≤ℕ/s : {m n : ℕ} -> m ¿≤ℕ n -> (succ m) ¿≤ℕ (succ n)

_-_ : (a : ℕ) -> (b : ℕ) -> {c : b ¿≤ℕ a} -> ℕ
_-_ m zero = m
_-_ zero (succ _) {}
_-_ (succ m) (succ n) {¿≤ℕ/s p} = _-_ m n {p}

Now the emacs interface to get the normal form of

zero - (succ zero) gives zero - (succ zero)
(succ zero) - zero gives succ zero
(succ zero) - (succ zero) fives (succ zero) - (succ zero)

but I can't fathom why.


I thought I would get what I expected this time.
I'm starting to become astonishingly confused.

-- 
Tristan Wibberley

Any opinion expressed is mine (or else I'm playing devils advocate for
the sake of a good argument). My employer had nothing to do with this
communication.