a6037b9 · Idris-dev · git.iko.soy

libs/base/Data/Fin.idr+1−1

compare with master

unifiedsplit

@@ -135,7 +135,7 @@ restrict n val = let val' = assert_total (abs (mod val (cast (S n)))) in

135 -- reasoning about primitives, so we need the

136 -- 'believe_me'. It's fine because val' must be

137 -- in the right range

138− fromInteger val'

138+ fromInteger {n = S n} val'

139 {prf = believe_me {a=IsJust (Just val')} ItIsJust}

140

141%language ErrorReflection

test/TestData.hs+2−1

@@ -76,7 +76,8 @@ testFamiliesData = [

76 ( 22, NODE_CG ),

77 ( 23, ANY ),

78 ( 24, ANY ),

79− ( 25, ANY )]),

79+ ( 25, ANY ),

80+ ( 26, ANY )]),

80 ("bignum", "Bignum",

81 ("bignum", "Bignum",

81 [ ( 1, ANY ),

82 [ ( 1, ANY ),

82 ( 2, ANY )]),

83 ( 2, ANY )]),

test/basic026/basic026.idrnew file+12

@@ -0,0 +1,12 @@

1+module Main

2+

3+import Data.Vect

4+

5+||| Verifies that `Fin.restrict` generates a valid `Fin`

6+||| by using it to index a `Vect`.

7+main : IO ()

8+main = 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'

12+

test/basic026/expectednew file+2

@@ -0,0 +1,2 @@

1+True

2+True

test/basic026/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ basic026.idr -o basic026

3+./basic026

4+rm -f basic026 *.ibc