Skip to content

Instantly share code, notes, and snippets.

@raichoo

raichoo/gist:9511511

Created March 12, 2014 17:09
Show Gist options
  • Save raichoo/9511511 to your computer and use it in GitHub Desktop.
Save raichoo/9511511 to your computer and use it in GitHub Desktop.
Download ZIP
Theorem of Choice
Raw
gistfile1.idr
choice : (R : a -> a -> Type) ->
((n : a) -> (m : a ** R n m)) ->
(f : (a -> a) ** (n : a) -> R n (f n))
choice R g = (\x => getWitness (g x) ** \y => getProof (g y))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment