jyapayne/ace
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

add a small demo for lean mode

Browse source
This commit is contained in:
Soonho Kong 2015-02-24 11:03:02 -05:00
commit 8f49d3d897
1 changed files with 9 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

9
demo/kitchen-sink/docs/lean.lean Normal file
View file

@ -0,0 +1,9 @@
import logic
section
variables (A : Type) (p q : A → Prop)
example : (∀x : A, p x ∧ q x) → ∀y : A, p y :=
assume H : ∀x : A, p x ∧ q x,
take y : A,
show p y, from and.elim_left (H y)
end