Skip to content

Instantly share code, notes, and snippets.

@konn

konn/russel.idr

Created February 26, 2014 15:20
Show Gist options
  • Save konn/9231436 to your computer and use it in GitHub Desktop.
Save konn/9231436 to your computer and use it in GitHub Desktop.
Download ZIP
Russel's paradox in idris.
Raw
russel.idr
russel : (P : a -> a -> Type) -> Exists _ (\y => (x : a) -> (P x y -> (P x x -> _|_), (P x x -> _|_) -> P x y)) -> _|_
russel P (x ** f) with (f x)
russel P (x ** f) | (a, b) = let a' = \x => a x x in a' (b a')
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment