Nontermination when reducing floats

Stream: lean4

[Logan Weber]

Hi all. I think I found a nontermination bug when inductive types have floats as indices. Code snippet:

inductive Test where
| c : Float → Test
#reduce Test.c 0.0

The reduce gives the following output:

maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)

Version:
Lean (version 4.0.0, commit 96de208a6b1a, Release)

I get the same behavior with structures too:

structure Test where
  (c : Float)
#reduce (⟨1.0⟩ : Test)

[Eric Wieser]

Is #reduce (1 : Float) ok?

[Logan Weber]

Oh. That doesn't terminate either. Looks like this has nothing to do with inductive types.

[Logan Weber]

(Changing topic name)

[Logan Weber]

Eval seems to be fine though:

#eval (1 : Float)