File size: 254 Bytes
0115dcf | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 | import Aesop
/-- Ensure that Aesop is running -/
example : α → α :=
by aesop
example : ∀ (p q: Prop), p ∨ q → q ∨ p := by
intro p q h
-- Here are some comments
cases h
. apply Or.inr
assumption
. apply Or.inl
assumption
|