string literal containing comment character

Stream: lean4

[Calvin Lee]

I may be missing something , but is there any way to do something like let s : String := "--help" ? since -- is a comment character this does not parse for me. Of course I can do "-" ++ "-help" but this seems somewhat unwieldy

[Julian Berman]

That particular example seems to work here I think -- on Lean (version 4.0.0, commit cc0712fc827f, Release)

[Julian Berman]

I #check "--help"     ■ "--help" : String

  def f : String :=
    let s : String := "--help"
    return s

I #eval f     ■ "--help"

[Julian Berman]

I noticed this I think for numbers though, that --2 is not - - 2 but yeah that one seems to work for me.

[Calvin Lee]

oh it might be my version then