Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC