git.iko.soy/Idris-dev
on master help sign in
Add test for preorder reasoning syntax
commitfc0a04c5920c04f96a2d1e8e55b06054c2eca052 authorDavid Christiansen <david@davidchristiansen.dk> dateSun 15 Dec 2013, 12:03 (13 years ago) parent6749dd5
4 files changed+15
compare with master
unifiedsplit
idris.cabal+3 test/test035/expected test/test035/run+3 test/test035/test035.idr+9
idris.cabal+3
@@ -284,6 +284,9 @@ Extra-source-files:
284284 test/test033/expected
285285 test/test034/run
286286 test/test034/expected
287+ test/test035/run
288+ test/test035/expected
289+ test/test035/*.idr
287290
288291source-repository head
289292 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