git.iko.soy/Idris-dev
on master help sign in
Add test for totality checking of partially applied function
commitdcaa109cd249f7bcb8316fccd98e855def482da8 authorAhmad Salim Al-Sibahi <asal@itu.dk> dateWed 15 Nov 2017, 18:28 (9 years ago) parent74214e6
3 files changed+11
compare with master
unifiedsplit
test/totality024/expected+1 test/totality024/run+3 test/totality024/totality023.idr+7
test/totality024/expectednew file+1
@@ -0,0 +1 @@
1+totality023.idr:5:3:Main.ana is possibly not total due to: Main.ana, go
test/totality024/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+${IDRIS:-idris} $@ totality023.idr --check
3+rm -f *.ibc
test/totality024/totality023.idrnew file+7
@@ -0,0 +1,7 @@
1+%default total
2+
3+mutual
4+ ana : (a -> Maybe a) -> a -> Nat
5+ ana f = go . f
6+ where go Nothing = Z
7+ go (Just x) = S $ ana f x