1
1
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-23 11:43:08 +03:00
Idris2/tests/idris2/basic044/Vec.idr
Guillaume ALLAIS 7ccc47712e [ re ] Better error messages in the REPL
(as well as in type signatures now that I know how to do that)
2021-02-19 12:34:19 +00:00

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]]