Add regression test
There no longer seems to be an issue for #3261, so it should be closed,
but a regression test would still be useful for it.
Fixes #3261
commit6404f9bcb7e445a7053447ced02ca92d2c2e3835
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateFri 10 Mar 2017, 14:31 (10 years ago)
parentad016d9
test/regression001/reg003.idrnew file+11
@@ -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 @@
11#!/usr/bin/env bash
22${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 \
45 reg047a.idr reg053.idr reg057.idr reg058.idr reg058a.idr \
56 reg059.idr reg060.idr reg061.idr reg062.idr reg063.idr \
67 reg064.idr reg065.idr reg066.idr reg071.idr reg074.idr \