git.iko.soy/Idris-dev
on 4994292 help sign in
Idris-dev/test/basic026/basic026.idr
12 lines 291 B history raw
1module Main
3import Data.Vect
5||| Verifies that `Fin.restrict` generates a valid `Fin`
6||| by using it to index a `Vect`.
7main : IO ()
8main = do
9 let xs = the (Vect 2 Char) ['a','b']
10 printLn $ Vect.index (restrict 1 0) xs == 'a'
11 printLn $ Vect.index (restrict 1 1) xs == 'b'