Auto-convert

lte10

module lte10 where

open import Data.Empty
open import Data.Unit
open import Data.Nat as ℕ
open import Data.Maybe
open import Data.Vec

open import Function

isJust : ∀ {A : Set} (ma : Maybe A) → Set
isJust (just x) = ⊤
isJust nothing  = ⊥

lte? : (m n : ℕ) → Maybe $ m ℕ.≤ n
lte? zero    n       = just z≤n
lte? (suc m) zero    = nothing
lte? (suc m) (suc n) with lte? m n
... | just pr = just (s≤s pr)
... | nothing = nothing

mkVec : ∀ n {m} {pr : isJust $ lte? m n} → Vec ℕ m → Vec ℕ n
mkVec n {m} {pr} xs with lte? m n
... | nothing  = ⊥-elim pr
... | just lte = helper lte xs
  where
    helper : ∀ {m n} (pr : m ℕ.≤ n) → Vec ℕ m → Vec ℕ n
    helper z≤n      xs       = replicate 0
    helper (s≤s pr) (x ∷ xs) = x ∷ helper pr xs

mkVec10 = mkVec 10

example : Vec ℕ 10
example = mkVec10 $ 1 ∷ 2 ∷ 3 ∷ []