2024-05-17 20:45:29 -07:00
|
|
|
|
import Aesop
|
2024-05-17 20:53:34 -07:00
|
|
|
|
|
2024-05-31 17:09:12 -07:00
|
|
|
|
/-- Ensure that Aesop is running -/
|
2024-05-17 20:53:34 -07:00
|
|
|
|
example : α → α :=
|
|
|
|
|
|
by aesop
|
2024-05-28 20:35:47 -07:00
|
|
|
|
|
|
|
|
|
|
example : ∀ (p q: Prop), p ∨ q → q ∨ p := by
|
|
|
|
|
|
intro p q h
|
2024-05-31 17:09:12 -07:00
|
|
|
|
-- Here are some comments
|
2024-05-28 20:35:47 -07:00
|
|
|
|
cases h
|
|
|
|
|
|
. apply Or.inr
|
|
|
|
|
|
assumption
|
|
|
|
|
|
. apply Or.inl
|
|
|
|
|
|
assumption
|
