[Agda] Unexpected successful loading of silly program

[Tristan Wibberley]

Hi all,

I changed the second clause of _-_ from:

_-_ zero (succ n) {}

to

_-_ zero (succ n) = zero

in this program:

http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php?n=Patterns.PartialFunction

however it then loaded successfully, furthermore, getting the canonical
form for zero - (succ zero) gives zero but I would have expected it to
fail. What does the {c : b ¿≤ℕ a} do exactly and why can I have an
absurd case if the type of the function is total after all?

On a related note how do I add a proof to my program that a function is
indeed partial to avoid errors which let it be total without noticing?


BTW, how do you get unicode characters into the wiki in preformatted
sections?

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