lean4-htt/tests
Scott Morrison 7cce64ee70
feat: omega doesn't check for defeq atoms (#3525)
```
example (a : Nat) :
    (((a + (2 ^ 64 - 1)) % 2 ^ 64 + 1) * 8 - 1 - (a + (2 ^ 64 - 1)) % 2 ^ 64 * 8 + 1) = 8 := by
  omega
```
used to time out, and now is fast.

(We will probably make separate changes later so the defeq checks would
be fast in any case here.)
2024-02-28 05:41:29 +00:00
..
bench chore: speedcenter: count max symbols in shared libraries (#3418) 2024-02-20 19:25:24 +00:00
compiler fix: split libInit_shared out of libleanshared (#3421) 2024-02-22 19:16:32 +00:00
elabissues
ir
lean feat: omega doesn't check for defeq atoms (#3525) 2024-02-28 05:41:29 +00:00
pkg
playground
plugin
simpperf
.gitignore
common.sh
lean-toolchain