d4d4ba6 · Idris-dev · git.iko.soy

idris.cabal+3

@@ -414,6 +414,9 @@ Extra-source-files:

414 test/directives001/*.idr

415 test/directives001/run

416 test/directives001/expected

417+ test/directives002/*.idr

418+ test/directives002/run

419+ test/directives002/expected

417

420

418 test/delab001/*.idr

421 test/delab001/*.idr

419 test/delab001/run

422 test/delab001/run

test/directives002/directives002.idrnew file+14

@@ -0,0 +1,14 @@

1+module directives002

2+

3+%access export

4+%default covering

5+

6+loop : ()

7+loop = loop

8+

9+namespace Main

10+ total

11+ main : IO ()

12+ main = do

13+ pure loop

14+ putStrLn $ "Hello World"

test/directives002/expectednew file+2

@@ -0,0 +1,2 @@

1+directives002.idr:12:3:

2+directives002.Main.main is possibly not total due to: directives002.loop

test/directives002/runnew file+4

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

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ directives002.idr --check --nocolour

3+

4+rm -f directives002 *.ibc