File tree Expand file tree Collapse file tree 2 files changed +4
-3
lines changed
Expand file tree Collapse file tree 2 files changed +4
-3
lines changed Original file line number Diff line number Diff line change @@ -17,8 +17,9 @@ leModulusDivisor :: forall a b. (1 <= b) => Dict (Mod a b + 1 <= b)
1717leModulusDivisor = unsafeCoerce (Dict :: Dict (0 <= 0 ))
1818
1919-- | if (1 <= a) and (1 <= b) then (1 <= DivRU a b)
20- strictlyPositiveDivRu :: forall a b . (1 <= a , 1 <= b ) => Dict (1 <= DivRU a b )
21- strictlyPositiveDivRu = unsafeCoerce (Dict :: Dict (0 <= 0 ))
20+ strictlyPositiveDivRu ::
21+ forall a b . (1 <= a , 1 <= b ) => Dict ((1 <= DivRU a b ) ~ (() :: Constraint ))
22+ strictlyPositiveDivRu = unsafeCoerce (Dict :: Dict (() ~ () ))
2223
2324-- | if (1 <= a) then (b <= ceil(b/a) * a)
2425leTimesDivRu :: forall a b . (1 <= a ) => Dict (b <= a * DivRU b a )
Original file line number Diff line number Diff line change @@ -358,7 +358,7 @@ packetizeFromDfT ::
358358 (KnownNat headerBytes ) =>
359359 (KnownNat dataWidth ) =>
360360 (1 <= dataWidth ) =>
361- (1 <= headerBytes `DivRU ` dataWidth ) =>
361+ (( 1 <= headerBytes `DivRU ` dataWidth ) ~ ( () :: Constraint ) ) =>
362362 ((dataWidth + 1 ) <= headerBytes ) =>
363363 -- | Mapping from `Df` input to output `_meta`
364364 (a -> metaOut ) ->
You can’t perform that action at this time.
0 commit comments