5d4d793 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

adjust test tutorial006 with --consolewidth for use with -f curses

5d4d793Andreas Reuleaux12 years ago

test/tutorial006/expected+2−1

@@ -10,7 +10,8 @@ When elaborating argument [95mxs[0m to constructor [91mData.VectType.Vect.::

10 [92mplus[0m [95mn[0m [95mn[0m

11 with

12 [92mplus[0m [95mn[0m [95mm[0m

13+tutorial006b.idr:10:10:

13−tutorial006b.idr:10:10:When elaborating right hand side of with block in Main.parity:

14+When elaborating right hand side of with block in Main.parity:

14Can't unify

15Can't unify

15 [94mParity[0m ([92mplus[0m ([91mS[0m [95mj[0m) ([91mS[0m [95mj[0m)) (Type of [91meven[0m)

16 [94mParity[0m ([92mplus[0m ([91mS[0m [95mj[0m) ([91mS[0m [95mj[0m)) (Type of [91meven[0m)

16with

17with

test/tutorial006/run+2−2

@@ -1,4 +1,4 @@

1#!/usr/bin/env bash

2−idris $@ tutorial006a.idr --check

2+idris --consolewidth 80 $@ tutorial006a.idr --check

3−idris $@ tutorial006b.idr --check

3+idris --consolewidth 80 $@ tutorial006b.idr --check

4rm -f *.ibc