[Agda] very basic question about False

[Dan Licata]

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