git.iko.soy/Idris-dev
on master help sign in
Add regression test
6404f9bEdwin Brady
test/regression001/reg003.idrnew file+11
compare with master
unifiedsplit
@@ -0,0 +1,11 @@
1+data Point : Num t => Nat -> t -> Type where
2+ Nil : Point Z t
3+
4+data Mono : (Monoid m) => () -> Type where
5+ Monono : (Monoid m) => Mono {m} ()
6+
7+data Mono1 : (Monoid m) => Type where
8+ Monono1 : (Monoid m) => Mono1 {m}
9+
10+data Mono2 : (m : Type) -> Monoid m => () -> Type where
11+ Monono2 : (Monoid m) => Mono2 m ()
test/regression001/run+2−1
@@ -1,6 +1,7 @@
1#!/usr/bin/env bash
1#!/usr/bin/env bash
2${IDRIS:-idris} $@ --check \
2${IDRIS:-idris} $@ --check \
3− reg001.idr reg002.idr reg036.idr reg037.idr reg038.idr reg046.idr \
3+ reg001.idr reg002.idr reg003.idr reg036.idr reg037.idr \
4+ reg038.idr reg046.idr \
4 reg047a.idr reg053.idr reg057.idr reg058.idr reg058a.idr \
5 reg047a.idr reg053.idr reg057.idr reg058.idr reg058a.idr \
5 reg059.idr reg060.idr reg061.idr reg062.idr reg063.idr \
6 reg059.idr reg060.idr reg061.idr reg062.idr reg063.idr \
6 reg064.idr reg065.idr reg066.idr reg071.idr reg074.idr \
7 reg064.idr reg065.idr reg066.idr reg071.idr reg074.idr \