Fix Fin literals and add test
This was actually due to a preview fix for a bug which we were working
around in Prelude.Fin! But the tests didn't catch the problem, and so
now they will in future.
commit246cdae4eb34b6dbc93ba7c68ccbf1f5a2d218d0
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateThu 30 Jan 2014, 16:34 (13 years ago)
parent6e1cac7
idris.cabal+3
@@ -203,6 +203,9 @@ Extra-source-files:
203203 test/reg031/run
204204 test/reg031/*.idr
205205 test/reg031/expected
206+ test/reg032/run
207+ test/reg032/*.idr
208+ test/reg032/expected
206209 test/test001/run
207210 test/test001/*.idr
208211 test/test001/expected
libs/prelude/Prelude/Fin.idr+1−1
@@ -77,7 +77,7 @@ data IsJust : Maybe a -> Type where
7777 ItIsJust : IsJust {a} (Just x)
7878
7979fromInteger : (x : Integer) ->
80− {default (ItIsJust _ _)
80+ {default ItIsJust
8181 prf : (IsJust (integerToFin x n))} -> Fin n
8282fromInteger {n} x {prf} with (integerToFin x n)
8383 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