[Agda] very basic question about False

[Vincent Siles]

Thanks a lot !

V.

2011/4/18 Dan Licata <drl at cs.cmu.edu>:
> Hi Vincent,
>
> You use an absurd pattern, which is written (), and then leave of the
> right-hand side:
>
> False_rec : (A : Set) -> False -> A
> False_rec A ()
>
> -Dan
>
> On Apr18, Vincent Siles wrote:
>> 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 ?
>>
>