We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 02b8b76 commit 8c04614Copy full SHA for 8c04614
tests/lean/run/issue10792.lean
@@ -4,5 +4,5 @@ inductive Vec (α : Type) : Nat → Type where
4
5
-- set_option trace.Meta.Match.match true
6
7
-def test : Vec Unit 10000 → Nat
+def test : Vec Unit 100000000000 → Nat
8
| Vec.cons () _ => 1
0 commit comments