mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-15 22:32:19 +03:00
22 lines
276 B
Idris
22 lines
276 B
Idris
module Vec
|
|
|
|
import Data.Fin
|
|
|
|
%default total
|
|
|
|
%logging 1
|
|
%logging "declare.def" 2
|
|
|
|
Vec : Type -> Nat -> Type
|
|
Vec a n = Fin n -> a
|
|
|
|
Nil : Vec a Z
|
|
Nil = absurd
|
|
|
|
(::) : a -> Vec a n -> Vec a (S n)
|
|
(x :: xs) FZ = x
|
|
(x :: xs) (FS i) = xs i
|
|
|
|
test : Vec (List Nat) 2
|
|
test = [[], [0]]
|