naturals

commit 8454395107598be25d3715db44f197f9cd43883b
parent 52cf94bf434c0fdb662380ab05a8c66463d76713
Author: Robert Russell <robert@rr3.xyz>
Date:   Sat,  5 Jul 2025 12:29:14 -0700

Add finatMirror and finaturalMirror

Diffstat:
M
src/Naturals/Finat.hs
 | 
4
+++-
M
src/Naturals/Finatural.hs
 | 
4
+++-

2 files changed, 6 insertions(+), 2 deletions(-)
diff --git a/src/Naturals/Finat.hs b/src/Naturals/Finat.hs
@@ -9,6 +9,7 @@ import Naturals.IsFin
 import Naturals.Nat
 import Naturals.Natural
 import Naturals.Peano
+import Naturals.Snat
 
 -- | Finite (@Peano@-indexed) prefixes of @Nat@.
 newtype Finat (n :: Peano) = FinatUnsafe Nat deriving newtype (Show, Eq)
@@ -29,4 +30,5 @@ instance IsFin Finat where
 
     finWeaken (FinatUnsafe n) = FinatUnsafe n
 
--- TODO: Special functions (e.g., mirror) for working with Snats and Finats together.
+finatMirror :: Snat n -> Finat n -> Finat n
+finatMirror (SnatUnsafe n) (FinatUnsafe i) = FinatUnsafe (n - i - 1)
diff --git a/src/Naturals/Finatural.hs b/src/Naturals/Finatural.hs
@@ -8,6 +8,7 @@ import Unsafe.Coerce
 import Naturals.IsFin
 import Naturals.Natural
 import Naturals.Peano
+import Naturals.Snatural
 
 -- | Finite (@Peano@-indexed) prefixes of @Natural@.
 newtype Finatural (n :: Peano) = FinaturalUnsafe Natural deriving newtype (Show, Eq)
@@ -25,4 +26,5 @@ instance IsFin Finatural where
 
     finWeaken (FinaturalUnsafe n) = FinaturalUnsafe n
 
--- TODO: Special functions (e.g., mirror) for working with Snaturals and Finaturals together.
+finaturalMirror :: Snatural n -> Finatural n -> Finatural n
+finaturalMirror (SnaturalUnsafe n) (FinaturalUnsafe i) = FinaturalUnsafe (n - i - 1)