ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-21 22:17:19 +03:00
Code Issues Projects Releases Wiki Activity

New regression test

Browse Source
This commit is contained in:
Edwin Brady 2014-07-16 21:05:14 +02:00
parent e6e1ad964a
commit 86ec4a1d58
5 changed files with 49 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
idris.cabal
View File

@ -238,6 +238,9 @@ Extra-source-files:
test/reg046/run
test/reg046/*.idr
test/reg046/expected
test/reg047/run
test/reg047/*.idr
test/reg047/expected
test/basic001/run
test/basic001/*.idr

0
test/reg047/expected Normal file
View File

18
test/reg047/reg047.idr Normal file
View File

@ -0,0 +1,18 @@
module test
data TTSigma : (A : Type) -> (B : A -> Type) -> Type where
sigma : (A : Type) -> (B : A -> Type) -> (a : A) -> B a -> TTSigma A B
data Nat = zero | succ Nat
Id : (A : Type) -> A -> A -> Type
Id A = (=) {a0 = A} {b0 = A}
Refl : (A : Type) -> (a : A) -> Id A a a
Refl A a = refl {a}
zzz : Id Nat zero zero
zzz = Refl Nat zero
eep : TTSigma Nat (\ a => Id Nat a zero)
eep = sigma Nat (\ a => Id Nat a zero) zero zzz

24
test/reg047/reg047a.idr Normal file
View File

@ -0,0 +1,24 @@
module test
data TTSigma : (A : Type) -> (B : A -> Type) -> Type where
sigma : (A : Type) -> (B : A -> Type) -> (a : A) -> B a -> TTSigma A B
data MNat = zero | succ MNat
Id : (A : Type) -> A -> A -> Type
Id = \A,x,y => x = y -- {a = A} {b = A}
Refl : (A : Type) -> (a : A) -> Id A a a
Refl A a = refl {a}
zzzz : Id MNat zero zero
zzzz = Refl MNat zero
eep : TTSigma MNat (\ c => Id MNat c zero)
eep = (sigma MNat (\b => Id MNat b zero) zero zzzz)
eep2 : TTSigma MNat (\ c => Id MNat c zero)
eep2 = (sigma MNat (\b => Id MNat b zero) zero (Refl MNat zero))

4
test/reg047/run Executable file
View File

@ -0,0 +1,4 @@
#!/usr/bin/env bash
idris $@ reg047.idr --check --nobuiltins
idris $@ reg047a.idr --check
rm -f *.ibc