module NonEmptyList where

infixr  _∷_

open import Data.Nat
open import Data.Fin

data NList (A : Set) : Set where
  [_] : A → NList A
  _∷_ : A → NList A → NList A

map : {A B : Set} → (f : A → B) → NList A → NList B
map f [ x ] = [ f x ]
map f (x ∷ l) = f x ∷ map f l

length : ∀ {A} → NList A → ℕ
length [ _ ] = 
length (_ ∷ l) = suc (length l)

Pos : {A : Set} → NList A → Set
Pos l = Fin (length l)