@@ -0,0 +1,29 @@
1+module TestLambdaImpossible
2+
3+%default total
4+
5+eqBool : (x, y : Bool) -> Dec (x = y)
6+eqBool False False = Yes Refl
7+eqBool False True = No (\(Refl) impossible)
8+eqBool True False = No (\(Refl) impossible)
9+eqBool True True = Yes Refl
10+
11+data Elem : {a : Type} -> a -> Prelude.List.List a -> Type where
12+ Here : {a : Type} -> {x : a} -> {xs : List a} -> Elem x (x :: xs)
13+ There : {a : Type} -> {x, y : a} -> {xs : List a} -> Elem x xs -> Elem x (y :: xs)
14+
15+notHereNotThere : Not (x = y) -> Not (Elem x xs) -> Not (Elem x (y :: xs))
16+notHereNotThere notEq notElem Here = notEq Refl
17+notHereNotThere notEq notElem (There elem) = notElem elem
18+
19+decElem : DecEq a => (x : a) -> (xs : List a) -> Dec (Elem x xs)
20+decElem x [] = No (\Here impossible)
21+decElem x (y :: xs) with (decEq x y)
22+ decElem x (x :: xs) | (Yes Refl) = Yes Here
23+ decElem x (y :: xs) | (No notHere) with (decElem x xs)
24+ decElem x (y :: xs) | (No notHere) | (Yes prf) = Yes (There prf)
25+ decElem x (y :: xs) | (No notHere) | (No notThere) = No $ notHereNotThere notHere notThere
26+
27+notEta : ((a : Type) -> (b : Type) -> (f : a -> b) -> f = (\x => f x)) -> Void
28+notEta eta = case eta Nat Nat id of
29+ Refl impossible