15 lines
310 B
Lean4
15 lines
310 B
Lean4
import Game.Metadata
|
||
|
||
example (a : ℕ) : a = 0 ∨ ¬ (a = 0) := by
|
||
by_cases h : a = 0
|
||
· left
|
||
exact h
|
||
· right
|
||
-- here the goal should show `h : a ≠ 0`
|
||
exact h
|
||
|
||
-- set_option pp.all true in
|
||
example (a : ℕ) : ¬ (a = 0) ↔ a ≠ 0 := by
|
||
-- both should be displayed the same way
|
||
rfl
|