Computation

Stream: general

[Sebastien Gouezel]

I was just playing with the continued fraction by @Kevin Kappelmann , which is very nice. And it computes well in the VM:

#eval (generalized_continued_fraction.of (121/98 : ℚ)).convergents 3

gives the answer 21/17 right away. Sadly,

example : ((generalized_continued_fraction.of (121/98 : ℚ)).convergents 3 = 21/17) := rfl

fails miserably, I guess because computing in unary is not a good idea. Apart from adding a specific module to norm_num or waiting for Lean 4, is there a way to get this automatically?

[Johan Commelin]

I guess the answer is by norm_num after the right simp-lemmas have been added.