module stlc.examples.product where open import Data.List open import stlc.term open import config open import stlc.catComb.compile open import stlc.run open Utils --- Example 1 - construct swapped pair --- ex1 : ∅ ⊢ nat × nat ex1 = (ƛ ƛ (# 1 , # 0)) · `nat 3 · `nat 4 inst1 : List Inst inst1 = compile ex1 x1 : Result x1 = run 100 ⟨ inst1 ∣ ⟨⟩ ∣ [] ⟩ --- Example 2 - swap pair ex2 : ∅ , (nat × nat) ⊢ nat × nat ex2 = snd (# 0) , fst (# 0) inst2 : List Inst inst2 = compile ex2 x2 : Result x2 = run 100 ⟨ inst2 ∣ ⟨⟩ , (`nat 1 , `nat 2) ∣ [] ⟩