a92f2f8 · Idris-dev · git.iko.soy

src/Idris/Termination.hs+1−1

@@ -429,7 +429,7 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

429 [ty] -> expand 0 (normalise (tt_ctxt ist) [] ty) args

430 _ -> args

431 where expand i (Bind n (Pi _ _ _ _) sc) (x : xs) = x : expand (i + 1) sc xs

432− expand i (Bind n (Pi _ _ _ _) sc) [] = Just (i, Same) : expand (i + 1) sc []

432+ expand i (Bind n (Pi _ _ _ _) sc) [] = Nothing : expand (i + 1) sc []

433 expand i _ xs = xs

434

435 mkChange n args pargs = [(n, expandToArity n (sizes args))]

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