open import Agda.Builtin.Nat using (Nat; _+_)

swapF : ∀ {A B : Set} → (A → A → B) → (A → A → B)
swapF f x y = f y x

testSwapAdd : Nat
testSwapAdd = swapF _+_  

testSwapAdd2 : Nat → Nat
testSwapAdd2 x = swapF _+_ x 

testSwapSwap : Nat
testSwapSwap = swapF (swapF _+_)  

add3 : Nat → Nat → (Nat → Nat)
add3 x y = λ z → x + y + z

testSwapAdd3 : Nat
testSwapAdd3 = swapF add3   

testSwapSwap3 : Nat
testSwapSwap3 = swapF (swapF add3)   

{-# FOREIGN AGDA2RUST
pub fn main() {
  println!("{}:\t {} | {} | {} | {} | {}", module_path!(),
    testSwapAdd(),
    testSwapAdd2(40),
    testSwapSwap(),
    testSwapAdd3(),
    testSwapSwap3(),
  );
}
#-}