git.iko.soy/Idris-dev
on master help sign in
New regression test
86ec4a1Edwin Brady
idris.cabal+3
compare with master
unifiedsplit
@@ -238,6 +238,9 @@ Extra-source-files:
238 test/reg046/run
238 test/reg046/run
239 test/reg046/*.idr
239 test/reg046/*.idr
240 test/reg046/expected
240 test/reg046/expected
241+ test/reg047/run
242+ test/reg047/*.idr
243+ test/reg047/expected
241
244
242 test/basic001/run
245 test/basic001/run
243 test/basic001/*.idr
246 test/basic001/*.idr
test/reg047/expectednew file

No changes to the content.

test/reg047/reg047.idrnew file+18
@@ -0,0 +1,18 @@
1+module test
2+
3+data TTSigma : (A : Type) -> (B : A -> Type) -> Type where
4+ sigma : (A : Type) -> (B : A -> Type) -> (a : A) -> B a -> TTSigma A B
5+
6+data Nat = zero | succ Nat
7+
8+Id : (A : Type) -> A -> A -> Type
9+Id A = (=) {a0 = A} {b0 = A}
10+
11+Refl : (A : Type) -> (a : A) -> Id A a a
12+Refl A a = refl {a}
13+
14+zzz : Id Nat zero zero
15+zzz = Refl Nat zero
16+
17+eep : TTSigma Nat (\ a => Id Nat a zero)
18+eep = sigma Nat (\ a => Id Nat a zero) zero zzz
test/reg047/reg047a.idrnew file+24
@@ -0,0 +1,24 @@
1+module test
2+
3+data TTSigma : (A : Type) -> (B : A -> Type) -> Type where
4+ sigma : (A : Type) -> (B : A -> Type) -> (a : A) -> B a -> TTSigma A B
5+
6+data MNat = zero | succ MNat
7+
8+Id : (A : Type) -> A -> A -> Type
9+Id = \A,x,y => x = y -- {a = A} {b = A}
10+
11+Refl : (A : Type) -> (a : A) -> Id A a a
12+Refl A a = refl {a}
13+
14+zzzz : Id MNat zero zero
15+zzzz = Refl MNat zero
16+
17+eep : TTSigma MNat (\ c => Id MNat c zero)
18+eep = (sigma MNat (\b => Id MNat b zero) zero zzzz)
19+
20+eep2 : TTSigma MNat (\ c => Id MNat c zero)
21+eep2 = (sigma MNat (\b => Id MNat b zero) zero (Refl MNat zero))
22+
23+
24+
test/reg047/runnew file+4
@@ -0,0 +1,4 @@
1+#!/usr/bin/env bash
2+idris $@ reg047.idr --check --nobuiltins
3+idris $@ reg047a.idr --check
4+rm -f *.ibc