toNat?

Stream: lean4

[Marcus Rossel]

Calling String.toNat?on the empty string yields some 0. Is this intended?
(Also, "".isNat evaluates to true).

[Henrik Böving]

I'm assuming you mean toNat?

[Marcus Rossel]

Henrik Böving said:

I'm assuming you mean toNat?

Yes, sorry - I've updated the title and question.

[Henrik Böving]

Looking at the implementation of both it comes down to isNat:

def isNat (s : String) : Bool :=
  s.all fun c => c.isDigit

def toNat? (s : String) : Option Nat :=
  if s.isNat then
    some <| s.foldl (fun n c => n*10 + (c.toNat - '0'.toNat)) 0
  else
    none

so one would have to add s.length > 0 to the isNat conditions.

[Sebastian Ullrich]

(or !s.isEmpty)

[Sebastian Ullrich]

fixed

[Marcus Rossel]

The same issue still exists for Substring:

def isNat (s : Substring) : Bool :=
  s.all fun c => c.isDigit

def toNat? (s : Substring) : Option Nat :=
  if s.isNat then
    some <| s.foldl (fun n c => n*10 + (c.toNat - '0'.toNat)) 0
  else
    none

Should this be adapted, too?

---

For comparison, here the implementation for String:

def isNat (s : String) : Bool :=
  !s.isEmpty && s.all (·.isDigit)

def toNat? (s : String) : Option Nat :=
  if s.isNat then
    some <| s.foldl (fun n c => n*10 + (c.toNat - '0'.toNat)) 0
  else
    none