2024-03-04 21:08:55 -08:00
|
|
|
|
@[export my_function]
|
|
|
|
|
|
def my_function (s: String): String :=
|
2024-03-07 21:37:37 -08:00
|
|
|
|
s ++ s!" at callee"
|
|
|
|
|
|
|
|
|
|
|
|
-- Formats a string in 3 different forms
|
|
|
|
|
|
@[export stylize]
|
|
|
|
|
|
def stylize (s: String): (String × String × String) :=
|
|
|
|
|
|
(s.capitalize, s.decapitalize, s.toUpper)
|
|
|
|
|
|
|
|
|
|
|
|
inductive Think where
|
|
|
|
|
|
| Success (s: String)
|
|
|
|
|
|
| Failure (i: Nat)
|
|
|
|
|
|
|
|
|
|
|
|
@[export think]
|
|
|
|
|
|
def think (s: String): Think :=
|
|
|
|
|
|
if s.front == 'S' then
|
|
|
|
|
|
Think.Success (s.drop 1)
|
|
|
|
|
|
else
|
|
|
|
|
|
Think.Failure s.length
|
