Skip to content

Instantly share code, notes, and snippets.

@zraffer

zraffer/foo.lean

Created March 17, 2016 15:38
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/291a6ea0841ed1955e5a to your computer and use it in GitHub Desktop.
Save zraffer/291a6ea0841ed1955e5a to your computer and use it in GitHub Desktop.
Download ZIP
lean issue
Raw
foo.lean
namespace foo
definition bool := ∀ a : Prop, a → a → a
definition tt : bool := λ (a : Prop) (c d : a), c
definition ff : bool := λ (a : Prop) (c d : a), d
definition ind_on_T := ∀ P : bool → Prop, ∀ a : bool, P tt → P ff → P a
definition ind_on : ind_on_T := λ (P : bool → Prop) (a : bool) (t : P tt) (f : P ff), a (P a) t f
check ind_on
end foo
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment