Zulip Chat Archive

Stream: new members

Topic: coercions between real and nat

Julia Ramos Alves (Jul 28 2022 at 15:49):

Hello there, I'm new at using Lean and I have a rather simple problem that I haven't yet been able to find a solution for. I'm trying to write an equality of real numbers but the terms for the left hand side are causing it to be interpreted as a natural number. How do I coerce it? I'm using division for it, is there some kind of "real division" I should be using instead?

David Renshaw (Jul 28 2022 at 15:54):

you can coerce like this: (x : ℝ)

David Renshaw (Jul 28 2022 at 15:54):

try doing that on some of the innermost terms

Julia Ramos Alves (Jul 28 2022 at 15:59):

the only variable that I had was just a sum index, so it had to be natural, but it seems like using "coe" works

Kevin Buzzard (Jul 28 2022 at 17:40):

@Julia Ramos Alves for reference: the best way to ask questions here is to post working code with all imports etc in it, so that other people can just cut and paste into VS Code and see the same problem as you. You'll then learn quickly that people usually give very efficient answers on this forum. See #mwe (that's a link) for more details on this technique.

Last updated: Dec 20 2023 at 11:08 UTC