lists of size at least n

atleastn.agda

open import Data.Nat

module atleastn (n : ℕ) {a} (A : Set a) where

open import Data.List using (List; length)
open import Data.Vec

record SizedList : Set a where
  field list : List A
        size : length list ≥ n

data Vec' : ℕ → Set a where
  mkVec′ : ∀ {m} → Vec A (m + n) → Vec' (m + n)

data WideVec : ∀ k → Vec A k → Set a where
  mkWideVec : ∀ {m} (xs : Vec A m) (ys : Vec A n) → WideVec (m + n) (xs ++ ys)

data InlinedWideVec : ℕ → Set a where
  rest : Vec A n → InlinedWideVec n
  _∷_  : ∀ {k} → A → InlinedWideVec k → InlinedWideVec (suc k)


open import Relation.Nullary.Decidable

record AtLeastN (m : ℕ) : Set a where
  field vec : Vec A m
        prf : m ≥ n

mkAtLeastN : ∀ {m} {p : True (n ≤? m)} → Vec A m → AtLeastN m
mkAtLeastN {m} {p} xs = record { vec = xs ; prf = toWitness p }