#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"