[Agda] Alternative partial function attempt

[Ulf Norell]

On Tue, Mar 25, 2008 at 2:19 AM, Tristan Wibberley <tristan at wibberley.org>
wrote:

> 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.


It's the same problem as before. The typechecker can't infer the less than
or equals proofs, since they are inductively defined. If you define them
recursively as I did in my example, it should work.

If you switch on the display of hidden arguments (C-c C-x C-h I think) it
might be easier to see what's going on.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080325/97d1bea5/attachment.html