246cdae · Idris-dev · git.iko.soy

idris.cabal+3

@@ -203,6 +203,9 @@ Extra-source-files:

203 test/reg031/run

204 test/reg031/*.idr

205 test/reg031/expected

206+ test/reg032/run

207+ test/reg032/*.idr

208+ test/reg032/expected

206 test/test001/run

209 test/test001/run

207 test/test001/*.idr

210 test/test001/*.idr

208 test/test001/expected

211 test/test001/expected

libs/prelude/Prelude/Fin.idr+1−1

@@ -77,7 +77,7 @@ data IsJust : Maybe a -> Type where

77 ItIsJust : IsJust {a} (Just x)

78

79fromInteger : (x : Integer) ->

80− {default (ItIsJust _ _)

80+ {default ItIsJust

81 prf : (IsJust (integerToFin x n))} -> Fin n

82fromInteger {n} x {prf} with (integerToFin x n)

83 fromInteger {n} x {prf = ItIsJust} | Just y = y

test/reg032/expectednew file

No changes to the content.

test/reg032/reg032.idrnew file+10

@@ -0,0 +1,10 @@

1+module reg032

2+

3+zfin : Fin 1

4+zfin = 0

5+

6+data Infer = MkInf a

7+

8+foo : Infer

9+foo = MkInf (the (Fin 1) 0)

10+

test/reg032/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris $@ reg032.idr --check

3+rm -f *.ibc