Skip to content

Commit

Permalink
[ upstream ] Remove use of a deprecated value
Browse files Browse the repository at this point in the history
  • Loading branch information
buzden committed Nov 28, 2024
1 parent b9751d9 commit d4cfb3c
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/Data/Nat1.idr
Original file line number Diff line number Diff line change
Expand Up @@ -85,7 +85,7 @@ gcd : (a, b : Nat) -> (0 ok : Either (IsSucc a) (IsSucc b)) => Nat1
gcd Z Z = void $ absurd ok
gcd a@(S _) Z = FromNat a
gcd Z b@(S _) = FromNat b
gcd a (S b) = assert_total $ gcd (S b) (modNatNZ a (S b) SIsNonZero)
gcd a (S b) = assert_total $ gcd (S b) (modNatNZ a (S b) %search)

export
gcd' : Nat1 -> Nat1 -> Nat1
Expand All @@ -109,4 +109,4 @@ normaliseWeights : Foldable f => Functor f => f (Nat1, a) -> f (Nat1, a)
normaliseWeights xs = do
let Just $ FromNat (S d) = foldmne gcd' $ Builtin.fst <$> xs
| Nothing => xs
flip map xs $ mapFst $ \(FromNat n) => FromNat (divNatNZ n (S d) SIsNonZero) @{believe_me $ ItIsSucc {n=1} {- since divisor is GCD -}}
flip map xs $ mapFst $ \(FromNat n) => FromNat (divNatNZ n (S d) %search) @{believe_me $ ItIsSucc {n=1} {- since divisor is GCD -}}

0 comments on commit d4cfb3c

Please sign in to comment.