Using `toExpr` to build an instance of \Q

Stream: lean4

[Ryan Ziegler]

When I have

#eval toExpr "1"

I get back a Lean.Expr.lit (Lean.Literal.strVal "1"), (which isn't technically wrong...) but I'd prefer to get back either a Nat or a Rational depending on what the string is. I'm coming up empty searching for the appropriate way to do this -- I can use toNat! if the string is always a Nat, but it might not be. Any pointers would be great! Thanks in advance!

[Mario Carneiro]

What do you expect in the Rat case?

[Eric Wieser]

toExpr takes a value an turns it into an expression; it sounds like you want to take source code and turn it into a value?

[Mario Carneiro]

perhaps something like this?

import Std.Data.Rat

def toNatOrRat (s : String) : Option (Nat ⊕ Rat) :=
  match s.toNat? with
  | some n => return .inl n
  | none => do
    let ⟨n, sign, e⟩ ← Lean.Syntax.decodeScientificLitVal? s
    return .inr <| Rat.ofScientific n sign e

#eval toNatOrRat "1" -- some (Sum.inl 1)
#eval toNatOrRat "1.0" -- some (Sum.inr 1)
#eval toNatOrRat "12.5" -- some (Sum.inr (25 : Rat)/2)

[Kyle Miller]

I guess if you want to support other bases there's also

#eval Lean.Syntax.decodeNatLitVal? "1" -- some 1
#eval Lean.Syntax.decodeNatLitVal? "0xFF" -- some 255