git.iko.soy/Idris-dev
on master help sign in
Improve the portability of reg041
1080689David Raymond Christiansen
test/reg041/expected+1−2
compare with master
unifiedsplit
@@ -1,4 +1,3 @@
1Type checking ./ott.idr
1Type checking ./ott.idr
2−?prf : (x : Bool) ->
3−(x1 : Bool) -> (El (EQ two x two x1)) -> El (EQ two x two x1)
2+?prf : (x : Bool) -> (x1 : Bool) -> (El (EQ two x two x1)) -> El (EQ two x two x1)
4Z
3Z
test/reg041/run+1−1
@@ -1,5 +1,5 @@
1#!/usr/bin/env bash
1#!/usr/bin/env bash
2−echo "example" | idris $@ --quiet ott.idr
2+idris $@ --quiet ott.idr -e example
3idris $@ showu.idr -o reg040
3idris $@ showu.idr -o reg040
4./reg040
4./reg040
5rm -f reg040 *.ibc
5rm -f reg040 *.ibc