3 lines
78 B
Text
3 lines
78 B
Text
@[export my_length]
|
|
def myLength (s : String) : UInt64 :=
|
|
s.length.toUInt64
|