git.iko.soy/Idris-dev
on master help sign in
Add test for preorder reasoning syntax
fc0a04cDavid Christiansen
idris.cabal+3
compare with master
unifiedsplit
@@ -284,6 +284,9 @@ Extra-source-files:
284 test/test033/expected
284 test/test033/expected
285 test/test034/run
285 test/test034/run
286 test/test034/expected
286 test/test034/expected
287+ test/test035/run
288+ test/test035/expected
289+ test/test035/*.idr
287
290
288source-repository head
291source-repository head
289 type: git
292 type: git
test/test035/expectednew file

No changes to the content.

test/test035/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+idris --check $@ test035.idr
3+rm -f *.ibc
test/test035/test035.idrnew file+9
@@ -0,0 +1,9 @@
1+module Main
2+
3+import Syntax.PreorderReasoning
4+import Control.Isomorphism
5+
6+stupidProof : Iso (Either a b) (Either a b)
7+stupidProof {a} {b} = (Either a b) ={ eitherComm }=
8+ (Either b a) ={ eitherComm }=
9+ (Either a b) QED