{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -Wno-overlapping-patterns -Wno-incomplete-patterns -Wno-incomplete-uni-patterns -fno-opt-coercion #-}
module Debug.RecoverRTTI.Tuple.Size (
ValidSize(..)
, TooBig(..)
, smallerIsValid
, IsValidSize(..)
, liftValidSize
, toValidSize
) where
import Data.Proxy
import Data.SOP.Dict
import Debug.RecoverRTTI.Nat
import Debug.RecoverRTTI.Util
data ValidSize (n :: Nat) where
ValidSize :: SNat n -> (forall r. TooBig n -> r) -> ValidSize n
smallerIsValid' :: forall n. ValidSize ('S n) -> ValidSize n
smallerIsValid' :: forall (n :: Nat). ValidSize ('S n) -> ValidSize n
smallerIsValid' = \(ValidSize (SS SNat n
n) forall r. TooBig ('S n) -> r
tooBig) -> forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize SNat n
n forall a b. (a -> b) -> a -> b
$ forall r. (TooBig ('S n) -> r) -> TooBig n -> r
aux forall r. TooBig ('S n) -> r
tooBig
where
aux :: (TooBig ('S n) -> r) -> TooBig n -> r
aux :: forall r. (TooBig ('S n) -> r) -> TooBig n -> r
aux TooBig ('S n) -> r
tooBig TooBig n
TooBig = TooBig ('S n) -> r
tooBig (forall (a :: Nat).
TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
a)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
TooBig :: TooBig ('S n))
smallerIsValid :: forall n r.
IsValidSize ('S n)
=> Proxy ('S n)
-> (IsValidSize n => r)
-> r
smallerIsValid :: forall (n :: Nat) r.
IsValidSize ('S n) =>
Proxy ('S n) -> (IsValidSize n => r) -> r
smallerIsValid Proxy ('S n)
_ IsValidSize n => r
k =
case forall (n :: Nat). ValidSize n -> Dict IsValidSize n
liftValidSize (forall (n :: Nat). ValidSize ('S n) -> ValidSize n
smallerIsValid' ValidSize ('S n)
valid) of
Dict IsValidSize n
Dict -> IsValidSize n => r
k
where
valid :: ValidSize ('S n)
valid :: ValidSize ('S n)
valid = forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize
class KnownNat n => IsValidSize n where
isValidSize :: ValidSize n
data TooBig (n :: Nat) where
TooBig :: TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S n)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
liftValidSize :: forall n. ValidSize n -> Dict IsValidSize n
liftValidSize :: forall (n :: Nat). ValidSize n -> Dict IsValidSize n
liftValidSize (ValidSize SNat n
n forall r. TooBig n -> r
notTooBig) = SNat n -> Dict IsValidSize n
go SNat n
n
where
go :: SNat n -> Dict IsValidSize n
go :: SNat n -> Dict IsValidSize n
go SNat n
SZ =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS SNat n
SZ) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS SNat n
SZ)) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS SNat n
SZ))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS SNat n
SZ)))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS SNat n
SZ))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS SNat n
SZ)))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))))))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))))))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))))))))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))))))))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
SZ)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SNat n
_))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
forall r. TooBig n -> r
notTooBig (forall (a :: Nat).
TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
a)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
TooBig :: TooBig n)
instance IsValidSize 'Z where
isValidSize :: ValidSize 'Z
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig 'Z -> r
\case
instance IsValidSize ('S 'Z) where
isValidSize :: ValidSize ('S 'Z)
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig ('S 'Z) -> r
\case
instance IsValidSize ('S ('S 'Z)) where
isValidSize :: ValidSize ('S ('S 'Z))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S 'Z)) -> r
\case
instance IsValidSize ('S ('S ('S 'Z))) where
isValidSize :: ValidSize ('S ('S ('S 'Z)))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S 'Z))) -> r
\case
instance IsValidSize ('S ('S ('S ('S 'Z)))) where
isValidSize :: ValidSize ('S ('S ('S ('S 'Z))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S 'Z)))) -> r
\case
instance IsValidSize ('S ('S ('S ('S ('S 'Z))))) where
isValidSize :: ValidSize ('S ('S ('S ('S ('S 'Z)))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S ('S 'Z))))) -> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S 'Z)))))) where
isValidSize :: ValidSize ('S ('S ('S ('S ('S ('S 'Z))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S ('S ('S 'Z)))))) -> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S 'Z))))))) where
isValidSize :: ValidSize ('S ('S ('S ('S ('S ('S ('S 'Z)))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S ('S ('S ('S 'Z))))))) -> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))) where
isValidSize :: ValidSize ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))) -> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))) where
isValidSize :: ValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))) -> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))) where
isValidSize :: ValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))) -> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))) where
isValidSize :: ValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))) where
isValidSize :: ValidSize
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))) where
isValidSize :: ValidSize
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S 'Z)))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S 'Z)))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))))))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))))))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-> r
\case
instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) where
isValidSize :: ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
isValidSize = forall (n :: Nat).
SNat n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize forall (n :: Nat). KnownNat n => SNat n
singNat forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-> r
\case
toValidSize :: Int -> Maybe (Some ValidSize)
toValidSize :: Int -> Maybe (Some ValidSize)
toValidSize = Int -> Maybe (Some ValidSize)
go
where
go :: Int -> Maybe (Some ValidSize)
go :: Int -> Maybe (Some ValidSize)
go Int
0 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @'Z
go Int
1 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S 'Z)
go Int
2 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S 'Z))
go Int
3 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S 'Z)))
go Int
4 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S 'Z))))
go Int
5 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S 'Z)))))
go Int
6 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S 'Z))))))
go Int
7 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S 'Z)))))))
go Int
8 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))
go Int
9 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))
go Int
10 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))
go Int
11 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))
go Int
12 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))
go Int
13 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))
go Int
14 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))
go Int
15 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))
go Int
16 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))
go Int
17 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))
go Int
18 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))
go Int
19 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))
go Int
20 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))
go Int
21 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))
go Int
22 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))
go Int
23 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))
go Int
24 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))
go Int
25 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))
go Int
26 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))
go Int
27 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))
go Int
28 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))
go Int
29 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))
go Int
30 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))
go Int
31 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))
go Int
32 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))
go Int
33 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))
go Int
34 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))
go Int
35 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))
go Int
36 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))
go Int
37 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))
go Int
38 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))
go Int
39 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))
go Int
40 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))
go Int
41 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))
go Int
42 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))
go Int
43 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))
go Int
44 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))
go Int
45 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))))
go Int
46 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))))
go Int
47 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))))))
go Int
48 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))))))
go Int
49 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))))))))
go Int
50 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))))))))
go Int
51 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))))))))))
go Int
52 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))))))))))
go Int
53 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))
go Int
54 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))
go Int
55 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))))
go Int
56 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))
go Int
57 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))))))
go Int
58 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
go Int
59 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
go Int
60 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
go Int
61 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
go Int
62 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Some f
Some forall a b. (a -> b) -> a -> b
$
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize @('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
go Int
_ = forall a. Maybe a
Nothing