| 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 | |
| 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 | |