## Stream: lean4

### Topic: string literal containing comment character

#### Calvin Lee (Mar 24 2021 at 19:55):

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 (Mar 24 2021 at 20:09):

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

#### Julian Berman (Mar 24 2021 at 20:09):

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

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

I #eval f     ■ "--help"


#### Julian Berman (Mar 24 2021 at 20:10):

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

#### Calvin Lee (Mar 24 2021 at 20:11):

oh it might be my version then

Last updated: May 18 2021 at 23:14 UTC