[ compat ] Use IsSucc instead of NonZero

frex-project · Oct 30, 2024 · 3707871 · 3707871
1 parent 213e508
commit 3707871
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 6 deletions.
diff --git a/tests/frextests/indexed-binary/Binary/Modular.idr b/tests/frextests/indexed-binary/Binary/Modular.idr
@@ -13,7 +13,7 @@ import Frexlet.Monoid.Commutative.Nat
 
 
 NZ2 : NonZero 2
-NZ2 = SIsNonZero
+NZ2 = %search
 
 export
 absurdSucIsZero : (k : Nat) -> (0 prf : S k = 0) -> b
@@ -68,14 +68,14 @@ multSucLeftCancel a b minusOne prf = multSucRightCancel a b minusOne $
   ~~ b * (S minusOne) ...(multCommutative _ _)
 
 export
-powerNZ : (n : Nat) -> NonZero (2 `power` n)
-powerNZ   0 = SIsNonZero
+powerNZ : (n : Nat) -> IsSucc (2 `power` n)
+powerNZ   0 = ItIsSucc
 powerNZ   (S n) with (powerNZ n)
  powerNZ  (S n) | prf with (2 `power` n)
-  powerNZ (S n) | SIsNonZero | S _ = SIsNonZero
+  powerNZ (S n) | ItIsSucc | S _ = ItIsSucc
 
 export
-modAffine : (a, k, n : Nat) -> (nz : NonZero n)
+modAffine : (a, k, n : Nat) -> (nz : IsSucc n)
          -> modNatNZ (n*k + a) n nz
           = modNatNZ        a  n nz
 modAffine a k n nz =

diff --git a/tests/frextests/indexed-binary/Binary/Properties.idr b/tests/frextests/indexed-binary/Binary/Properties.idr
@@ -105,7 +105,7 @@ numCarryUnique
           ~~ val'                            ...(sym $ valueFord_x)
           ~~ val_y + (2 `power` width) * c_y ...(      valueFord_y)
           ~~ c_y * (2 `power` width) + val_y ...(sym $ lemma c_y (2 `power` width) val_y)
-        0 powern_neq_zero : NonZero (2 `power` width)
+        0 powern_neq_zero : IsSucc (2 `power` width)
         powern_neq_zero = powerNZ width
         0 val_x_lt_2n : val_x `LT` (2 `power` width)
         val_x_lt_2n = bitsBound num_x