# [Agda] hidden proofs

Sergei Meshveliani mechvel at botik.ru
Tue Jul 30 20:57:34 CEST 2013

```On Wed, 2013-07-31 at 03:46 +1000, Liam O'Connor wrote:
> Hi Sergei,
>
>
> I was pretty easily able to define "even" using a similar definition
>
>
> open import Data.Nat
>
>
> mutual
>  data Even : ℕ → Set
>   where
>    even0 : Even 0
>    even-suc : {n : ℕ} → Even n → Even (suc (suc n))
>
>
> open import Relation.Nullary
>
>
> even : (n : ℕ) -> Dec (Even n)
> even zero = yes even0
> even (suc zero) = no (λ ()) -- absurd pattern :)
> even (suc (suc n)) with even n
> ... | yes p = yes (even-suc p)
> ... | no p = no (λ { (even-suc x) → p x })
>

Great! Thank you. A good point for me.

Initially I also had this precise definition of Even.
But I was stupid enough and has not guessed that  even (suc 0)
is an absurd pattern here.

There remains a (beginner) question here:
how does the programmer know which pattern the type checker will agree
to qualify as absurd?
This is a matter of the Language definition.

If the checker was only for this example with Even, then all right,
there is a clear special algorithm.
But suppose that one defines

data Foo : ℕ → Set where
foo1 : Bool -> (n : ℕ) → Foo n
foo2 : <something complex>
...
foo9 : ... -> Foo (f n)

foo? : ℕ → Dec \$ Foo n
foo? 100 = no (λ ())
...

How does the checker decide on whether  foo? 100
is an absurd pattern or not?

Thanks,

------
Sergei

```