git.iko.soy/Idris-dev
on master help sign in
Add test for totality checking of partially applied function
dcaa109Ahmad Salim Al-Sibahi
test/totality024/expectednew file+1
compare with master
unifiedsplit
@@ -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