feat: allow numeric literals to be coerced to option type

[robsimmons]

This PR allows adds new instances for the OfNat and OfScientific typeclass that allow numeric literals to be treated as having Option type.

This change fixes an apparent asymmetry between numerals and other Lean expressions. Thanks to the optionCoe typeclass, an expression that synthesizes the type α can be coerced to Option α. However, a numeral like 5 or 4.2e3 does not synthesize the type Nat or Float because it expands to e.g. OfNat.ofNat (α := _) (nat_lit 5), and typeclass inference will fail to find an instance that lets α be an Option type.

Comparing this with the behavior of String makes the apparent asymmetry particularly egregious, because string literals don't get a similar typeclass wrapper.

def s : String := "4"
example : Option String := s
example : Option String := ("3" : String)
example : Option String := "3"

def n : Nat := 4
example : Option Nat := n
example : Option Nat := (3 : Nat)
example : Option Nat := 3 -- Fails currently, succeeds under this PR

def d : Float := 4.
example : Option Float := d
example : Option Float := (3. : Float)
example : Option Float := 3. -- Fails currently, succeeds under this PR

Despite these instances not being coercions, the effect is quite similar to the optionCoe typeclass that defines the coercion α → Option α, so by putting them in Init.Data.Option.Core we ensure that these instances are similarly banned inside Init and Std.

https://live.lean-lang.org/#codez=CYUwZgBAzhBcEGUAuAnAlgOwOZwLwQCIAWAgKBAA8BDAWwAcAbEOCAeTqTQHsNFVMcsfFHLV6TFu048+6bHggAKAgGYCLZHKwBKUbUbN4U7r00CFqsqVCRe8AHJUkConvGG2HExEfOhEDDcDSS8ZXwVFFRZfXUp9CSNQ3nD/KIBaNIgAMSo0BhgAYwBXFBQQDCQGAE8AGmgigoKQEGAYIoxQFAgkAAs0GAAFACVSa3AIYBYshi4nFwA6IITPaV5p2b98YCWPYxl1uf9I+amZp1ixYMTV7LPNiBUTjOzc/Ihi0vLK2vrG5taIO1Ot0+oMhkA

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6d5efd79b9d751a487c4b3049e283fc412b0179e --onto ac0b82933f6eac9914011ca2caf38d0e4e991160. You can force Mathlib CI using the force-mathlib-ci label. (2025-09-27 05:11:37)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5d3df7b5f45fa4781edd56c9b8869c49f89b820c --onto 0b2193c7715a55246d0596a4db548c1b5b81562a. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-03 18:02:44)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 6d5efd79b9d751a487c4b3049e283fc412b0179e --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-09-27 05:11:39)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 5d3df7b5f45fa4781edd56c9b8869c49f89b820c --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-03 18:02:46)

[david-christiansen]

I wouldn't refer to this as a coercion - I think it's more accurate to say "this instance enables natural number literals for Option when the contained type has natural number literals."

The interactions between coercions, overloaded literals, and type-based disambiguation are a bit subtle, and we don't do users a favor by being imprecise in our use of language and terminology.

[robsimmons]

I agree with your call for precision of language here. Your suggestion works, but I feel like it's missing a meaningful verb. To put that a different way, there's a Mad Lib I would like to complete that looks like this:

This change allows natural number literals to [be?] [to/as?] Option A type whenever A is an allowed(?) type for that natural number literal.

You're making a very reasonable object to "to be coerced to." What about "to be promoted to", or "to be cast to". Or given your comment about denotation, perhaps "interpret" is a good verb that is close to "denote"

This change allows natural number literals to be interpreted as values of type Option A type whenever that literal could also be interpreted as a value of type A.

Would that make sense and capture the core meaning of your more accurate statement?

[david-christiansen]

I think the key thing to have here is that natural number literals don't really start off as a Nat to be later transformed into some other type, but rather guide the initial elaboration of the value. Your second text captures that well.

I don't think the docs should say "this change", though - that's a good PR description, but the docs should describe the software as it is, not as it was or is becoming.

Also, is "interpret" the right verb here? It's not terrible, but it's also highly overloaded (we're not invoking the interpreter here). What about this:

This allows natural number literals to be used for Option types. In particular, if the literal n
can be used for type α, then it can also be used for Option α, with the value wrapped in some.

[robsimmons]

"Used" seems more overloaded to me than "interpret," and with less helpfully-leading semantic content. "Treat?"

This allows Lean to treat a natural number literal as an expression that has an Option type. In particular, if Lean knows how to treat the natural number n as an expression that has type α, then Lean can also treat n as a expression with type Option α by adding an additional Option.some.

[robsimmons]

Making this a real PR, though there's no urgency of merging it until @kim-em is back in town and caught up.