lean4-htt/tests/elab_bench/big_struct.lean
Garmelon 08eb78a5b2
chore: switch to new test/bench suite (#12590)
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.
2026-02-25 13:51:53 +00:00

205 lines
2.7 KiB
Text

set_option maxRecDepth 1_000_000
set_option maxHeartbeats 0
structure M where
b0 : Unit
b1 : Unit
b2 : Unit
b3 : Unit
b4 : Unit
b5 : Unit
b6 : Unit
b7 : Unit
b8 : Unit
b9 : Unit
b10 : Unit
b11 : Unit
b12 : Unit
b13 : Unit
b14 : Unit
b15 : Unit
b16 : Unit
b17 : Unit
b18 : Unit
b19 : Unit
b20 : Unit
b21 : Unit
b22 : Unit
b23 : Unit
b24 : Unit
b25 : Unit
b26 : Unit
b27 : Unit
b28 : Unit
b29 : Unit
b30 : Unit
b31 : Unit
b32 : Unit
b33 : Unit
b34 : Unit
b35 : Unit
b36 : Unit
b37 : Unit
b38 : Unit
b39 : Unit
b40 : Unit
b41 : Unit
b42 : Unit
b43 : Unit
b44 : Unit
b45 : Unit
b46 : Unit
b47 : Unit
b48 : Unit
b49 : Unit
b50 : Unit
b51 : Unit
b52 : Unit
b53 : Unit
b54 : Unit
b55 : Unit
b56 : Unit
b57 : Unit
b58 : Unit
b59 : Unit
b60 : Unit
b61 : Unit
b62 : Unit
b63 : Unit
b64 : Unit
b65 : Unit
b66 : Unit
b67 : Unit
b68 : Unit
b69 : Unit
b70 : Unit
b71 : Unit
b72 : Unit
b73 : Unit
b74 : Unit
b75 : Unit
b76 : Unit
b77 : Unit
b78 : Unit
b79 : Unit
b80 : Unit
b81 : Unit
b82 : Unit
b83 : Unit
b84 : Unit
b85 : Unit
b86 : Unit
b87 : Unit
b88 : Unit
b89 : Unit
b90 : Unit
b91 : Unit
b92 : Unit
b93 : Unit
b94 : Unit
b95 : Unit
b96 : Unit
b97 : Unit
b98 : Unit
b99 : Unit
b100 : Unit
b101 : Unit
b102 : Unit
b103 : Unit
b104 : Unit
b105 : Unit
b106 : Unit
b107 : Unit
b108 : Unit
b109 : Unit
b110 : Unit
b111 : Unit
b112 : Unit
b113 : Unit
b114 : Unit
b115 : Unit
b116 : Unit
b117 : Unit
b118 : Unit
b119 : Unit
b120 : Unit
b121 : Unit
b122 : Unit
b123 : Unit
b124 : Unit
b125 : Unit
b126 : Unit
b127 : Unit
b128 : Unit
b129 : Unit
b130 : Unit
b131 : Unit
b132 : Unit
b133 : Unit
b134 : Unit
b135 : Unit
b136 : Unit
b137 : Unit
b138 : Unit
b139 : Unit
b140 : Unit
b141 : Unit
b142 : Unit
b143 : Unit
b144 : Unit
b145 : Unit
b146 : Unit
b147 : Unit
b148 : Unit
b149 : Unit
b150 : Unit
b151 : Unit
b152 : Unit
b153 : Unit
b154 : Unit
b155 : Unit
b156 : Unit
b157 : Unit
b158 : Unit
b159 : Unit
b160 : Unit
b161 : Unit
b162 : Unit
b163 : Unit
b164 : Unit
b165 : Unit
b166 : Unit
b167 : Unit
b168 : Unit
b169 : Unit
b170 : Unit
b171 : Unit
b172 : Unit
b173 : Unit
b174 : Unit
b175 : Unit
b176 : Unit
b177 : Unit
b178 : Unit
b179 : Unit
b180 : Unit
b181 : Unit
b182 : Unit
b183 : Unit
b184 : Unit
b185 : Unit
b186 : Unit
b187 : Unit
b188 : Unit
b189 : Unit
b190 : Unit
b191 : Unit
b192 : Unit
b193 : Unit
b194 : Unit
b195 : Unit
b196 : Unit
b197 : Unit
b198 : Unit
b199 : Unit