[Agda] very basic question about False

Vincent Siles vincent.siles at ens-lyon.org
Mon Apr 18 18:42:44 CEST 2011


Hi,
I just started to play a bit with Agda, and I wonder how
can I define the following function:

data False where

False_rec : (A : Set) -> False -> A
False_rec A f = **stuck**

Is there a way to pattern match against False
to kill a goal ?

Cheers,
Vincent


More information about the Agda mailing list