Skip to content

Commit

Permalink
Add equals# for Fin#
Browse files Browse the repository at this point in the history
  • Loading branch information
andrewthad committed Nov 2, 2024
1 parent f999770 commit dfb16bf
Showing 1 changed file with 7 additions and 1 deletion.
8 changes: 7 additions & 1 deletion src/Arithmetic/Fin.hs
Original file line number Diff line number Diff line change
Expand Up @@ -65,6 +65,9 @@ module Arithmetic.Fin
, fromInt#
, constant#

-- * Compare
, equals#

-- * Lift and Unlift
, lift
, unlift
Expand All @@ -75,7 +78,7 @@ import Prelude hiding (last, succ)
import Arithmetic.Nat ((<?))
import Arithmetic.Types (Difference (..), Fin (..), Nat, Nat#, pattern MaybeFinJust#, pattern MaybeFinNothing#, type (:=:), type (<), type (<#), type (<=))
import Arithmetic.Unsafe (Fin# (Fin#), MaybeFin#, Nat# (Nat#))
import GHC.Exts (Int (I#), Int#, Word#, (+#))
import GHC.Exts (Int (I#), Int#, Word#, (+#), (==#))
import GHC.TypeNats (CmpNat, type (+))

import qualified Arithmetic.Equal as Eq
Expand Down Expand Up @@ -610,3 +613,6 @@ type applications to clarify when it is helpful. For example:
-}
constant# :: forall (b :: GHC.Nat) (a :: GHC.Nat). (CmpNat a b ~ 'LT) => Nat# a -> Fin# b
constant# (Nat# i) = Fin# i

equals# :: Fin# n -> Fin# n -> Bool
equals# (Fin# a) (Fin# b) = Exts.isTrue# (a ==# b)

0 comments on commit dfb16bf

Please sign in to comment.