mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
a3cb39eac9
This PR migrates most remaining tests to the new test suite. It also completes the migration of directories like `tests/lean/run`, meaning that PRs trying to add tests to those old directories will now fail.
36 lines
621 B
Lean4
36 lines
621 B
Lean4
|
||
def hello : (x : Nat) → (h : x = x) → True := by
|
||
intro x
|
||
--^ goals
|
||
intro
|
||
--^ goals
|
||
trivial
|
||
|
||
def hello2 : (x : Nat) → (h : x = x) → True := by
|
||
intros
|
||
--^ goals
|
||
trivial
|
||
|
||
|
||
theorem qqww (x y : Nat) (f : (α → x = y)) (h : y = x) : True := by
|
||
rw [h] at f
|
||
--^ goals
|
||
trivial
|
||
|
||
theorem qqww2 (x y : Nat) (f : (α → x = y)) (h : y = x) : True := by
|
||
rw [h] at f
|
||
--^ goals
|
||
trivial
|
||
|
||
theorem adsf : (True ∧ True) := by
|
||
apply And.intro
|
||
--^ goals
|
||
trivial
|
||
--^ goals
|
||
trivial
|
||
--^ goals
|
||
|
||
theorem comm (x y z : Nat) (h : y = x) : (x + z) = (z + y) := by
|
||
rw [Nat.add_comm, h]
|
||
--^ goals
|