Skip to content

Instantly share code, notes, and snippets.

@larrytheliquid

larrytheliquid/CrazyNames.agda

Last active December 12, 2015 07:18
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save larrytheliquid/4735146 to your computer and use it in GitHub Desktop.
Save larrytheliquid/4735146 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
CrazyNames.agda
open import Data.Bool
open import Data.Nat
open import Data.String
module CrazyNames where
data U : Set where
`Bool `ℕ : U
El : U → Set
El `Bool = Bool
El `ℕ = ℕ
var : U → String
var `Bool = "b"
var `ℕ = "n"
show : (u : U) → (var u : El u) → String
show `Bool b = {!!}
show `ℕ n = {!!}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment