Merge pull request #29 from stefan-hoeck/total

[ compat ] temporary fix for idris issue 2954
stefan-hoeck · Apr 25, 2023 · 80a7c46 · 80a7c46
2 parents 8080c4b + 3b97f2d
commit 80a7c46
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 2 deletions.
diff --git a/src/Algebra/Solver/Ring/Sum.idr b/src/Algebra/Solver/Ring/Sum.idr
@@ -107,6 +107,7 @@ normalize e = normSum (norm e)
 --------------------------------------------------------------------------------
 
 -- Adding two sums via `add` preserves the evaluation result.
+-- Note: `assert_total` in here is a temporary fix for idris issue #2954
 0 padd :  SolvableRing a
        => (x,y : Sum a as)
        -> esum x + esum y === esum (add x y)
@@ -125,7 +126,7 @@ padd (T m x :: xs) (T n y :: ys) with (compProd x y) proof eq
     ~~ n * eprod y + ((m * eprod x + esum xs) + esum ys)
        ..< p213
     ~~ n * eprod y + esum (add (T m x :: xs) ys)
-       ... cong (n * eprod y +) (padd (T m x :: xs) ys)
+       ... cong (n * eprod y +) (assert_total $ padd (T m x :: xs) ys)
 
   _ | EQ = case pcompProd x y eq of
         Refl => Calc $

diff --git a/src/Algebra/Solver/Semiring/Sum.idr b/src/Algebra/Solver/Semiring/Sum.idr
@@ -93,6 +93,7 @@ normalize e = normSum (norm e)
 --------------------------------------------------------------------------------
 
 -- Adding two sums via `add` preserves the evaluation result.
+-- Note: `assert_total` in here is a temporary fix for idris issue #2954
 0 padd :  SolvableSemiring a
        => (x,y : Sum a as)
        -> esum x + esum y === esum (add x y)
@@ -111,7 +112,7 @@ padd (T m x :: xs) (T n y :: ys) with (compProd x y) proof eq
     ~~ n * eprod y + ((m * eprod x + esum xs) + esum ys)
        ..< p213
     ~~ n * eprod y + esum (add (T m x :: xs) ys)
-       ... cong (n * eprod y +) (padd (T m x :: xs) ys)
+       ... cong (n * eprod y +) (assert_total $ padd (T m x :: xs) ys)
 
   _ | EQ = case pcompProd x y eq of
         Refl => Calc $