Skip to content

Instantly share code, notes, and snippets.

@brunoczim

brunoczim/Tuple.agda

Created December 2, 2018 02:06
Show Gist options
  • Save brunoczim/44c2d36bec67332e5af799ec8de01b3a to your computer and use it in GitHub Desktop.
Save brunoczim/44c2d36bec67332e5af799ec8de01b3a to your computer and use it in GitHub Desktop.
Download ZIP
Tuple with generic length in Agda
Raw
Tuple.agda
module Tuple
open import Data.Vec
open import Agda.Builtin.Nat renaming (Nat to ℕ)
data Tuple : {n : ℕ} → Vec Set n → Set where
∅ : Tuple []
_,_ : {A : Set} {n : ℕ} {v : Vec Set n} → A → Tuple v → Tuple (A ∷ v)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment