mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
20 lines
459 B
Plaintext
20 lines
459 B
Plaintext
issue3232.lean:5:2-5:9: error: Tactic `apply` failed: could not unify the type of `h`
|
|
@foo 42
|
|
with the goal
|
|
@foo 23
|
|
|
|
h : foo
|
|
⊢ foo
|
|
issue3232.lean:8:2-8:29: error: Tactic `apply` failed: could not unify the type of `rfl`
|
|
(1 : Int) = 1
|
|
with the goal
|
|
(1 : Nat) = 1
|
|
|
|
⊢ 1 = 1
|
|
issue3232.lean:11:2-11:25: error: Tactic `apply` failed: could not unify the type of `Eq.refl PUnit`
|
|
Eq.{2} PUnit PUnit
|
|
with the goal
|
|
Eq.{1} PUnit PUnit
|
|
|
|
⊢ PUnit = PUnit
|