[Agda-dev] One more point for my false-golfing score

[Andreas Abel]

-- https://code.google.com/p/agda/issues/detail?id=1599

data ⊥ : Set where

abstract

   T : Set → Set
   T X = X → ⊥

   data D : Set where
     lam : T D → D

   app : D → D → ⊥
   app (lam f) = f

   omega : D
   omega = lam λ x → app x x

   Omega : ⊥
   Omega = app omega omega

absurd : ⊥
absurd = Omega

-- Horray!

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/