Skip to content

Instantly share code, notes, and snippets.

@gallais
Created May 2, 2014 14:55
Show Gist options
  • Save gallais/8e2a0baa879206b782c4 to your computer and use it in GitHub Desktop.
Save gallais/8e2a0baa879206b782c4 to your computer and use it in GitHub Desktop.
Auto-convert
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 ∷ []
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment