mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-11-11 03:34:13 +03:00
adjust test tutorial006 with --consolewidth for use with -f curses
This commit is contained in:
parent
2a7d6a96b9
commit
5d4d793186
@ -10,7 +10,8 @@ When elaborating argument [95mxs[0m to constructor [91mData.VectType.Vect.::
|
||||
[92mplus[0m [95mn[0m [95mn[0m
|
||||
with
|
||||
[92mplus[0m [95mn[0m [95mm[0m
|
||||
tutorial006b.idr:10:10:When elaborating right hand side of with block in Main.parity:
|
||||
tutorial006b.idr:10:10:
|
||||
When elaborating right hand side of with block in Main.parity:
|
||||
Can't unify
|
||||
[94mParity[0m ([92mplus[0m ([91mS[0m [95mj[0m) ([91mS[0m [95mj[0m)) (Type of [91meven[0m)
|
||||
with
|
||||
|
@ -1,4 +1,4 @@
|
||||
#!/usr/bin/env bash
|
||||
idris $@ tutorial006a.idr --check
|
||||
idris $@ tutorial006b.idr --check
|
||||
idris --consolewidth 80 $@ tutorial006a.idr --check
|
||||
idris --consolewidth 80 $@ tutorial006b.idr --check
|
||||
rm -f *.ibc
|
||||
|
Loading…
Reference in New Issue
Block a user