mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-15 22:32:19 +03:00
22 lines
274 B
Idris
22 lines
274 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]]
|