Hypothesis causes an infinite loop in the VM

Stream: general

[Eric Wieser]

In #13894, I have a function signature that looks like:

def fractional_digits (n : ℕ) (hn : 1 < n) (r : R) (hr : true → 0 ≤ r) (k : ℕ) : fin n :=

which I can #eval just fine. If I remove the true → , then I get a determistic timeout. What's going on here? Why is a proof argument affecting the runtime behavior?

[Kyle Miller]

I just tried it without the true ->, and it seems to work fine for me

#eval (list.range 10).map (fractional_digits 10 (by norm_num) (1/7 : ℚ) (by norm_num))
-- [1, 4, 2, 8, 5, 7, 1, 4, 2, 8]

[Eric Wieser]

Huh, that eval works. This is the one (from the PR) that fails:

#eval fractional_digits 10 (by norm_num) (0.12345 : ℚ) (by norm_num) ∘ (coe : fin 15 → ℕ)