From 20173c939486ed6e27b8170e94f666d8ae3df152 Mon Sep 17 00:00:00 2001 From: Tom Smeding Date: Thu, 13 Jun 2024 13:09:04 +0200 Subject: Rename *LengthSNat to *Rank --- test/Gen.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'test') diff --git a/test/Gen.hs b/test/Gen.hs index 559fecf..695b83f 100644 --- a/test/Gen.hs +++ b/test/Gen.hs @@ -101,7 +101,7 @@ genReplicatedShR = \m n -> do where injectOnes :: m <= n => SNat n -> IShR m -> IShR m -> Gen (IShR n, IShR n) injectOnes n@SNat shOnes sh - | m@SNat <- shrLengthSNat sh + | m@SNat <- shrRank sh = case cmpNat n m of LTI -> error "unreachable" EQI -> return (shOnes, sh) @@ -161,7 +161,7 @@ genPerm n@SNat k = do list <- forAll $ genPermR (fromSNat' n) permFromList list $ \perm -> do case permCheckPermutation perm $ - case sameNat' (permLengthSNat perm) n of + case sameNat' (permRank perm) n of Just Refl -> Just (k perm) Nothing -> Nothing of -- cgit v1.2.3-70-g09d2