dagit · March 10, 2019 08:32 · canonic-epicure · May 18, 2018 · canonic-epicure · May 18, 2018
diff --git a/HList.agda b/HList.agda
 module HList where

 open import Level
 open import Data.Bool
 open import Data.Nat hiding (_⊔_)
 open import Data.Vec
 open import Data.List

 data HList {a} : List (Set a) → Set (Level.suc a) where
  []  : HList []
  _∷_ : {HeadT : Set a}{TailT : List (Set a)}
        (x : HeadT) (xs : HList TailT) → HList (HeadT ∷ TailT)

 data HVec {a} : (n : ℕ) → Vec (Set a) n → Set (Level.suc a) where
  []  : HVec 0 []
  _∷_ : ∀{m}{HeadT : Set a}{TailT : Vec (Set a) m}
        (x : HeadT) (xs : HVec m TailT) → HVec (ℕ.suc m) (HeadT ∷ TailT) 

 test₁ : HVec 3 (Bool ∷ ℕ ∷ List Bool ∷ [])
 test₁ = true ∷ 5 ∷ (true ∷ false ∷ []) ∷ []

 test₂ : HList (Vec ℕ 1 ∷ ℕ ∷ Bool ∷ [])
 test₂ = x ∷ 0 ∷ true ∷ []
  where
  x : Vec ℕ 1
  x = 1 ∷ []

 {-
 These are simpler definitions if you prefer not to deal with levels.

 data HList : List Set → Set₁ where
  []  : HList []
  _∷_ : {HeadT : Set }{TailT : List Set}
        (x : HeadT) (xs : HList TailT) → HList (HeadT ∷ TailT)

 data HVec : (n : ℕ) → Vec Set n → Set₁ where
  []  : HVec 0 [] 
  _∷_ : ∀{m}{HeadT : Set }{TailT : Vec Set m}
        (x : HeadT) (xs : HVec m TailT) → HVec (ℕ.suc m) (HeadT ∷ TailT) 
 -}
	module HList where

	open import Level
	open import Data.Bool
	open import Data.Nat hiding (_⊔_)
	open import Data.Vec
	open import Data.List

	data HList {a} : List (Set a) → Set (Level.suc a) where
	[] : HList []
	_∷_ : {HeadT : Set a}{TailT : List (Set a)}
	(x : HeadT) (xs : HList TailT) → HList (HeadT ∷ TailT)

	data HVec {a} : (n : ℕ) → Vec (Set a) n → Set (Level.suc a) where
	[] : HVec 0 []
	_∷_ : ∀{m}{HeadT : Set a}{TailT : Vec (Set a) m}
	(x : HeadT) (xs : HVec m TailT) → HVec (ℕ.suc m) (HeadT ∷ TailT)

	test₁ : HVec 3 (Bool ∷ ℕ ∷ List Bool ∷ [])
	test₁ = true ∷ 5 ∷ (true ∷ false ∷ []) ∷ []

	test₂ : HList (Vec ℕ 1 ∷ ℕ ∷ Bool ∷ [])
	test₂ = x ∷ 0 ∷ true ∷ []
	where
	x : Vec ℕ 1
	x = 1 ∷ []

	{-
	These are simpler definitions if you prefer not to deal with levels.

	data HList : List Set → Set₁ where
	[] : HList []
	_∷_ : {HeadT : Set }{TailT : List Set}
	(x : HeadT) (xs : HList TailT) → HList (HeadT ∷ TailT)

	data HVec : (n : ℕ) → Vec Set n → Set₁ where
	[] : HVec 0 []
	_∷_ : ∀{m}{HeadT : Set }{TailT : Vec Set m}
	(x : HeadT) (xs : HVec m TailT) → HVec (ℕ.suc m) (HeadT ∷ TailT)
	-}
No results found