git.iko.soy/Idris-dev

on master help sign in

test/quasiquote004/expected+2−1

@@ -1,2 +1,3 @@

1−Quasiquote004.idr:50:25:When elaborating right hand side of Quasiquote004.getMeNat':

1+Quasiquote004.idr:50:25:

2+When elaborating right hand side of Quasiquote004.getMeNat':

23Not a Nat goal

test/quasiquote004/run+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−idris $@ --check --nocolour Quasiquote004.idr

2+idris --consolewidth 80 $@ --check --nocolour Quasiquote004.idr

33rm -f *.ibc

test/reg003/run+2−2

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

11#!/usr/bin/env bash

2−idris --check reg003.idr

3−idris --check reg003a.idr

2+idris --consolewidth 80 --check reg003.idr

3+idris --consolewidth 80 --check reg003a.idr

44rm -f *.ibc

test/reg006/expected+2−1

@@ -1 +1,2 @@

1−reg006.idr:17:1:RBTree.lookup is possibly not total due to: RBTree.case block in lookup

1+reg006.idr:17:1:

2+RBTree.lookup is possibly not total due to: RBTree.case block in lookup

test/reg006/run+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−idris $@ reg006.idr --check

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

33rm -f *.ibc