module stlc.inst where

open import Data.Nat using (ℕ)
open import Data.List

data Inst : Set where
  UNIT : Inst
  NAT : ℕ → Inst
  SKIP : Inst
  FST : Inst
  SND : Inst
  APP : Inst
  CUR : List Inst → Inst
  PUSH : Inst
  SWAP : Inst
  PAIR : Inst
--- COPRODUCT ---
  INL : Inst
  INR : Inst
  CASE : List Inst → List Inst → Inst
--- LIST OBJECT ---
  NIL : Inst
  C : Inst
  IT : List Inst → List Inst → Inst