module compilers where

module 1960s where
  open import Agda.Builtin.Nat using (_+_ ; _*_)
  open import Agda.Builtin.Equality using (_≡_ ; refl)
  _ : 5 + 6 ≡ 11
  _ = refl

module 1950s where
  open import Agda.Builtin.Nat using (Nat)
  bipush : Nat → Nat
  bipush x = x

  open import Agda.Builtin.Nat renaming (_+_ to iadd)
  open import Agda.Builtin.Equality using (_≡_ ; refl)
  _ : iadd (bipush 5) (bipush 6) ≡ 11
  _ = refl