blob: 5c0d3a9a504e4c16d5bc4e0d4fa22b9317f000a2 [file] [edit]
#eval Lean.Name.mkStr (Lean.Name.mkNum `foo 2) "bla"
#eval `foo.bla
#eval Lean.Name.anonymous
#eval Lean.Name.mkNum Lean.Name.anonymous 11
#eval Lean.Name.mkNum `foo.bla 5
#eval Lean.Name.mkStr Lean.Name.anonymous "abc"
#eval Lean.Name.mkStr Lean.Name.anonymous "--->"
#eval Lean.Name.mkStr Lean.Name.anonymous "2"