Idris2/tests/idris2/total001/Total.idr

%default partial

data Vect : Nat -> Type -> Type where
     Nil : Vect Z a
     (::) : a -> Vect k a -> Vect (S k) a

data Fin : Nat -> Type where
     FZ : Fin (S k)
     FS : Fin k -> Fin (S k)

lookup : Fin n -> Vect n a -> a
lookup FZ (x :: xs) = x
lookup (FS k) (x :: xs) = lookup k xs

lookup' : Fin n -> Vect n a -> a
lookup' (FS k) (x :: xs) = lookup' k xs

lookup'' : Fin n -> Vect n a -> a
lookup'' n xs = lookup' n xs
All functions now need to be covering by default This has caught a couple of things in the Idris 2 code base itself. Some tests needed partial annotations too. 2020-05-24 21:58:20 +03:00			`%default partial`

Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here! 2020-05-19 20:25:18 +03:00			`data Vect : Nat -> Type -> Type where`
			`Nil : Vect Z a`
			`(::) : a -> Vect k a -> Vect (S k) a`

			`data Fin : Nat -> Type where`
			`FZ : Fin (S k)`
			`FS : Fin k -> Fin (S k)`

			`lookup : Fin n -> Vect n a -> a`
			`lookup FZ (x :: xs) = x`
			`lookup (FS k) (x :: xs) = lookup k xs`

			`lookup' : Fin n -> Vect n a -> a`
			`lookup' (FS k) (x :: xs) = lookup' k xs`

			`lookup'' : Fin n -> Vect n a -> a`
			`lookup'' n xs = lookup' n xs`