[Agda] Absurd pattern in implicit argument of a lambda abstraction

[Dan Doel]

On Tuesday 02 November 2010 1:16:35 pm Florent Balestrieri wrote:
> When an expression of type "{Empty} -> A -> B" is expected, it is not
> possible to write:
> (\ {()})
> 
> Instead, it is necessary to name a function.
> f : {Empty} -> A -> B
> f {()}

  data ⊥ : Set where

  data Code : Set where
    bot : Code

  decode : Code → Set
  decode bot = ⊥

  foo : ∀{R : Set} → (c : Code) → ((∀{A : Set} → {v : decode c} → A) → R) → R
  foo bot k = k (λ{A} {})

\{} is the implicit absurd lambda, not \{()}.

-- Dan