Skip to content

Instantly share code, notes, and snippets.

@pnlph

pnlph/compilers.agda

Last active May 7, 2020 15:55
Show Gist options
  • Save pnlph/0917aea6b634b56bcced03564d3e5784 to your computer and use it in GitHub Desktop.
Save pnlph/0917aea6b634b56bcced03564d3e5784 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
compilers.agda
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment