blob: 838fe3658dae3dc13b98bc8fa925b38333e743e6 [file] [edit]
Lean.Name.mkStr1 "foo" : Lean.Name
Lean.Name.mkStr2 "foo" "bla" : Lean.Name
Lean.Name.mkStr1 "foo bla" : Lean.Name
Lean.Name.mkStr2 "foo bla" "hello world" : Lean.Name
Lean.Name.mkStr3 "foo bla" "boo" "hello world" : Lean.Name
Lean.Name.mkStr2 "foo" "hello" : Lean.Name
Lean.Name.mkStr1 "hello" : Lean.Name
Lean.Name.mkStr2 "hello" "world !!!" : Lean.Name