832c7412d6
@Kha It has a few advantages over `<or>` (`<|>`).
- It is not an infix operator.
- It takes tactic sequences instead of tactics as arguments
For example, we can write
```
first
| apply h1; assumption
| exact y; exact h3; assumption
```
or
```
first apply h1; assumption | exact y; exact h3; assumption
```
instead of
```
(apply h1; assumption) <|> (exact y; exact h3; assumption)
```
60 lines
1.5 KiB
Text
60 lines
1.5 KiB
Text
inductive Weekday where
|
||
| sunday : Weekday
|
||
| monday : Weekday
|
||
| tuesday : Weekday
|
||
| wednesday : Weekday
|
||
| thursday : Weekday
|
||
| friday : Weekday
|
||
| saturday : Weekday
|
||
|
||
def Weekday.next : Weekday -> Weekday :=
|
||
fun d => match d with
|
||
| sunday => monday
|
||
| monday => tuesday
|
||
| tuesday => wednesday
|
||
| wednesday => thursday
|
||
| thursday => friday
|
||
| friday => saturday
|
||
| saturday => sunday
|
||
|
||
def Weekday.previous : Weekday -> Weekday
|
||
| sunday => saturday
|
||
| monday => sunday
|
||
| tuesday => monday
|
||
| wednesday => tuesday
|
||
| thursday => wednesday
|
||
| friday => thursday
|
||
| saturday => friday
|
||
|
||
theorem Weekday.nextOfPrevious (d : Weekday) : next (previous d) = d := by
|
||
cases d
|
||
allGoals rfl
|
||
|
||
theorem Weekday.nextOfPrevious' (d : Weekday) : previous (next d) = d ∧ next (previous d) = d := by
|
||
apply And.intro
|
||
cases d <;> rfl
|
||
cases d <;> rfl
|
||
|
||
theorem Weekday.nextOfPrevious'' (d : Weekday) : previous (next d) = d ∧ next (previous d) = d := by
|
||
apply And.intro <;> cases d <;> rfl
|
||
|
||
open Lean.Parser.Tactic in
|
||
macro "rwd " x:term : tactic => `(rw $x:term; done)
|
||
|
||
theorem ex (a b c : α) (h₁ : a = b) (h₂ : a = c) : b = a ∧ c = a := by
|
||
apply And.intro <;> first rwd h₁ | rwd h₂
|
||
|
||
theorem idEq (a : α) : id a = a :=
|
||
rfl
|
||
|
||
theorem Weekday.test (d : Weekday) : next (previous d) = id d := by
|
||
cases d
|
||
traceState
|
||
allGoals rw idEq
|
||
traceState
|
||
allGoals rfl
|
||
|
||
theorem Weekday.test2 (d : Weekday) : next (previous d) = id d := by
|
||
cases d <;> rw idEq
|
||
traceState
|
||
allGoals rfl
|