RustCallLean/Callee/Callee.lean

4 lines
76 B
Plaintext
Raw Normal View History

2024-03-04 21:08:55 -08:00
@[export my_function]
def my_function (s: String): String :=
s ++ s!"abc"