Skip to content

Instantly share code, notes, and snippets.

@zraffer

zraffer/Prop

Created March 17, 2016 10:35
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save zraffer/ee04c6ee3b0d6cf4947f to your computer and use it in GitHub Desktop.
Save zraffer/ee04c6ee3b0d6cf4947f to your computer and use it in GitHub Desktop.
Download ZIP
errorneous attempt for boolean eliminator
Raw
bool
-- #bool
∀ (a : #Prop ) → a → a → a
Raw
ff
-- #ff
λ (a : #Prop ) → λ (c : a) → λ (d : a) → d
Raw
ind_on
-- #ind_on
λ (P : #bool → #Prop ) → λ (t : P #tt ) → λ (f : P #ff ) → λ (a : #bool ) → a (P a) t f
Raw
ind_on_T
-- #ind_on_T
∀ (P : #bool → #Prop ) → P #tt → P #ff → ∀ (a : #bool ) → P a
Raw
ind_on_test
-- #ind_on_test
(\(t : #ind_on_T ) → t) #ind_on
Raw
Prop
-- #Prop
*
Raw
tt
-- #tt
λ (a : #Prop ) → λ (c : a) → λ (d : a) → c
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment