search

nomeata / loogle

Mathlib search tool
https://loogle.lean-lang.org/
Apache License 2.0
50 stars 6 forks source link

Investigate why `123` leads to deterministic timeout #3

Open nomeata opened 8 months ago

nomeata commented 8 months ago

Probably some Nat constant that is expensive to evaluate.

vherrmann commented 2 months ago

There's also deterministic timeout on things like "|- ?a = -(-?a)" or "|- ?a = (?a⁻¹)⁻¹":

(deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached
use `set_option maxHeartbeats <num>` to set the limit
use `set_option diagnostics true` to get diagnostic information