/-  Clara Löh; 10/2023 -/

def f : Nat → Nat → Nat 
:= λ x => (λ y => x + 2 * y)
-- λ x y => x + 2 * y 

#check f 2                 -- Nat → Nat
#eval (f 2) 20             -- 42
#check (f 3) ∘ (f 2)       -- Nat → Nat
#eval ((f 3) ∘ (f 2)) 504  -- 2023

open List
open Char
open String

def g : String → String
:= asString
∘ reverse 
∘ (filter (λ x => not (x ∈ ['a','e','i','o','u'])) ) 
∘ map (λ x => if x == 'x' then 'u' else x) 
∘ map (λ x => if x == 'u' then 'x' else x)
∘ map toLower
∘ toList

#eval toString "Tux"
#eval asString ['T','u','x']
#eval g "Tux ist ein Pinguin"

def g' : String → String
:= asString
∘ reverse 
∘ (filter (λ x => not (x ∈ ['a','e','i','o','u','x'])) ) 
∘ map toLower
∘ toList

#eval g' "Tux ist ein Pinguin"  -- "ngnp n ts t"