{-# 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.Util
import Debug.RecoverRTTI.Util.TypeLevel
data ValidSize (n :: Nat) where
ValidSize :: Sing n -> (forall r. TooBig n -> r) -> ValidSize n
smallerIsValid' :: forall n. ValidSize ('S n) -> ValidSize n
smallerIsValid' :: ValidSize ('S n) -> ValidSize n
smallerIsValid' = \(ValidSize (SS n) forall r. TooBig ('S n) -> r
tooBig) -> Sing n -> (forall r. TooBig n -> r) -> ValidSize n
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing n
n ((forall r. TooBig n -> r) -> ValidSize n)
-> (forall r. TooBig n -> r) -> ValidSize n
forall a b. (a -> b) -> a -> b
$ (TooBig ('S n) -> r) -> TooBig n -> r
forall r. (TooBig ('S n) -> r) -> TooBig n -> r
aux TooBig ('S n) -> r
forall r. TooBig ('S n) -> r
tooBig
where
aux :: (TooBig ('S n) -> r) -> TooBig n -> r
aux :: (TooBig ('S n) -> r) -> TooBig n -> r
aux TooBig ('S n) -> r
tooBig TooBig n
TooBig = TooBig ('S n) -> r
tooBig (TooBig ('S n)
forall (n :: 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
n)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
TooBig :: TooBig ('S n))
smallerIsValid :: forall n r.
IsValidSize ('S n)
=> Proxy ('S n)
-> (IsValidSize n => r)
-> r
smallerIsValid :: Proxy ('S n) -> (IsValidSize n => r) -> r
smallerIsValid Proxy ('S n)
_ IsValidSize n => r
k =
case ValidSize n -> Dict IsValidSize n
forall (n :: Nat). ValidSize n -> Dict IsValidSize n
liftValidSize (ValidSize ('S n) -> ValidSize n
forall (n :: Nat). ValidSize ('S n) -> ValidSize n
smallerIsValid' ValidSize ('S n)
valid) of
Dict IsValidSize n
Dict -> r
IsValidSize n => r
k
where
valid :: ValidSize ('S n)
valid :: ValidSize ('S n)
valid = ValidSize ('S n)
forall (n :: Nat). IsValidSize n => ValidSize n
isValidSize
class SingI 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 :: ValidSize n -> Dict IsValidSize n
liftValidSize (ValidSize Sing n
n forall r. TooBig n -> r
notTooBig) = Sing n -> Dict IsValidSize n
go Sing n
n
where
go :: Sing n -> Dict IsValidSize n
go :: Sing n -> Dict IsValidSize n
go Sing n
SZ =
Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS SZ) =
Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS SZ)) =
Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS SZ))) =
Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS SZ)))) =
Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS SZ))))) =
Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS SZ)))))) =
Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS SZ))))))) =
Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS SZ)))))))) =
Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ))))))))) =
Dict IsValidSize n
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
go (SS (SS (SS (SS (SS (SS (SS (SS (SS (SS SZ)))))))))) =
Dict IsValidSize n
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 SZ))))))))))) =
Dict IsValidSize n
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 SZ)))))))))))) =
Dict IsValidSize n
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 SZ))))))))))))) =
Dict IsValidSize n
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 SZ)))))))))))))) =
Dict IsValidSize n
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 SZ))))))))))))))) =
Dict IsValidSize n
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 SZ)))))))))))))))) =
Dict IsValidSize n
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 SZ))))))))))))))))) =
Dict IsValidSize n
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 SZ)))))))))))))))))) =
Dict IsValidSize n
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 SZ))))))))))))))))))) =
Dict IsValidSize n
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 SZ)))))))))))))))))))) =
Dict IsValidSize n
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 SZ))))))))))))))))))))) =
Dict IsValidSize n
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 SZ)))))))))))))))))))))) =
Dict IsValidSize n
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 SZ))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ)))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ))))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ)))))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ))))))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ)))))))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ))))))))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ)))))))))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ))))))))))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ)))))))))))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ))))))))))))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ)))))))))))))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ))))))))))))))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ)))))))))))))))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ))))))))))))))))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ)))))))))))))))))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ))))))))))))))))))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ)))))))))))))))))))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ))))))))))))))))))))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ)))))))))))))))))))))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ))))))))))))))))))))))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ)))))))))))))))))))))))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ))))))))))))))))))))))))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ)))))))))))))))))))))))))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ))))))))))))))))))))))))))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ)))))))))))))))))))))))))))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ))))))))))))))))))))))))))))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ)))))))))))))))))))))))))))))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ))))))))))))))))))))))))))))))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ)))))))))))))))))))))))))))))))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ))))))))))))))))))))))))))))))))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ)))))))))))))))))))))))))))))))))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ)))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ))))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ)))))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
Dict IsValidSize n
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 SZ)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
Dict IsValidSize n
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 _))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) =
TooBig n -> Dict IsValidSize n
forall r. TooBig n -> r
notTooBig (TooBig n
forall (n :: 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
n)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
TooBig :: TooBig n)
instance IsValidSize 'Z where
isValidSize :: ValidSize 'Z
isValidSize = Sing 'Z -> (forall r. TooBig 'Z -> r) -> ValidSize 'Z
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing 'Z
forall k (a :: k). SingI a => Sing a
sing ((forall r. TooBig 'Z -> r) -> ValidSize 'Z)
-> (forall r. TooBig 'Z -> r) -> ValidSize 'Z
forall a b. (a -> b) -> a -> b
$ TooBig 'Z -> r
forall r. TooBig 'Z -> r
\case
instance IsValidSize ('S 'Z) where
isValidSize :: ValidSize ('S 'Z)
isValidSize = Sing ('S 'Z)
-> (forall r. TooBig ('S 'Z) -> r) -> ValidSize ('S 'Z)
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing ('S 'Z)
forall k (a :: k). SingI a => Sing a
sing ((forall r. TooBig ('S 'Z) -> r) -> ValidSize ('S 'Z))
-> (forall r. TooBig ('S 'Z) -> r) -> ValidSize ('S 'Z)
forall a b. (a -> b) -> a -> b
$ TooBig ('S 'Z) -> r
forall r. TooBig ('S 'Z) -> r
\case
instance IsValidSize ('S ('S 'Z)) where
isValidSize :: ValidSize ('S ('S 'Z))
isValidSize = Sing ('S ('S 'Z))
-> (forall r. TooBig ('S ('S 'Z)) -> r) -> ValidSize ('S ('S 'Z))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing ('S ('S 'Z))
forall k (a :: k). SingI a => Sing a
sing ((forall r. TooBig ('S ('S 'Z)) -> r) -> ValidSize ('S ('S 'Z)))
-> (forall r. TooBig ('S ('S 'Z)) -> r) -> ValidSize ('S ('S 'Z))
forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S 'Z)) -> r
forall r. TooBig ('S ('S 'Z)) -> r
\case
instance IsValidSize ('S ('S ('S 'Z))) where
isValidSize :: ValidSize ('S ('S ('S 'Z)))
isValidSize = Sing ('S ('S ('S 'Z)))
-> (forall r. TooBig ('S ('S ('S 'Z))) -> r)
-> ValidSize ('S ('S ('S 'Z)))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing ('S ('S ('S 'Z)))
forall k (a :: k). SingI a => Sing a
sing ((forall r. TooBig ('S ('S ('S 'Z))) -> r)
-> ValidSize ('S ('S ('S 'Z))))
-> (forall r. TooBig ('S ('S ('S 'Z))) -> r)
-> ValidSize ('S ('S ('S 'Z)))
forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S 'Z))) -> r
forall r. TooBig ('S ('S ('S 'Z))) -> r
\case
instance IsValidSize ('S ('S ('S ('S 'Z)))) where
isValidSize :: ValidSize ('S ('S ('S ('S 'Z))))
isValidSize = Sing ('S ('S ('S ('S 'Z))))
-> (forall r. TooBig ('S ('S ('S ('S 'Z)))) -> r)
-> ValidSize ('S ('S ('S ('S 'Z))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing ('S ('S ('S ('S 'Z))))
forall k (a :: k). SingI a => Sing a
sing ((forall r. TooBig ('S ('S ('S ('S 'Z)))) -> r)
-> ValidSize ('S ('S ('S ('S 'Z)))))
-> (forall r. TooBig ('S ('S ('S ('S 'Z)))) -> r)
-> ValidSize ('S ('S ('S ('S 'Z))))
forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S 'Z)))) -> r
forall r. 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 = Sing ('S ('S ('S ('S ('S 'Z)))))
-> (forall r. TooBig ('S ('S ('S ('S ('S 'Z))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S 'Z)))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing ('S ('S ('S ('S ('S 'Z)))))
forall k (a :: k). SingI a => Sing a
sing ((forall r. TooBig ('S ('S ('S ('S ('S 'Z))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S 'Z))))))
-> (forall r. TooBig ('S ('S ('S ('S ('S 'Z))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S 'Z)))))
forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S ('S 'Z))))) -> r
forall r. 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 = Sing ('S ('S ('S ('S ('S ('S 'Z))))))
-> (forall r. TooBig ('S ('S ('S ('S ('S ('S 'Z)))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S ('S 'Z))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing ('S ('S ('S ('S ('S ('S 'Z))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r. TooBig ('S ('S ('S ('S ('S ('S 'Z)))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S ('S 'Z)))))))
-> (forall r. TooBig ('S ('S ('S ('S ('S ('S 'Z)))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S ('S 'Z))))))
forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S ('S ('S 'Z)))))) -> r
forall r. 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 = Sing ('S ('S ('S ('S ('S ('S ('S 'Z)))))))
-> (forall r. TooBig ('S ('S ('S ('S ('S ('S ('S 'Z))))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S ('S ('S 'Z)))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing ('S ('S ('S ('S ('S ('S ('S 'Z)))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r. TooBig ('S ('S ('S ('S ('S ('S ('S 'Z))))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S ('S ('S 'Z))))))))
-> (forall r. TooBig ('S ('S ('S ('S ('S ('S ('S 'Z))))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S ('S ('S 'Z)))))))
forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S ('S ('S ('S 'Z))))))) -> r
forall r. 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 = Sing ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))
-> (forall r.
TooBig ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r. TooBig ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))
-> (forall r.
TooBig ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))
forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))) -> r
forall r. 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 = Sing ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))
-> (forall r.
TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))
-> (forall r.
TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))
forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))) -> r
forall r.
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 = Sing ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))
-> (forall r.
TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))
-> (forall r.
TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))) -> r)
-> ValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))
forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))) -> r
forall r.
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 = Sing ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))
-> (forall r.
TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))
-> r)
-> ValidSize
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))
-> r)
-> ValidSize
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))
-> (forall r.
TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))
-> r)
-> ValidSize
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))
forall a b. (a -> b) -> a -> b
$ TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))
-> r
forall r.
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 = Sing ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))
-> (forall r.
TooBig
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))
-> r)
-> ValidSize
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
TooBig
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))
-> r)
-> ValidSize
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))
-> (forall r.
TooBig
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))
-> r)
-> ValidSize
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))
forall a b. (a -> b) -> a -> b
$ TooBig
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))
-> r
forall r.
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 = Sing
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))
-> (forall r.
TooBig
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))
-> r)
-> ValidSize
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
TooBig
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))
-> r)
-> ValidSize
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))
-> (forall r.
TooBig
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))
-> r)
-> ValidSize
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))
forall a b. (a -> b) -> a -> b
$ TooBig
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))
-> r
forall r.
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 = Sing
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))
-> (forall r.
TooBig
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))
-> r)
-> ValidSize
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
TooBig
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))
-> r)
-> ValidSize
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))
-> (forall r.
TooBig
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))
-> r)
-> ValidSize
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))
forall a b. (a -> b) -> a -> b
$ TooBig
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))
-> r
forall r.
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 = Sing
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))
-> (forall r.
TooBig
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))
-> r)
-> ValidSize
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
TooBig
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))
-> r)
-> ValidSize
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))
-> (forall r.
TooBig
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))
-> r)
-> ValidSize
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))
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
forall r.
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 = Sing
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))
-> (forall r.
TooBig
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))
-> r)
-> ValidSize
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
TooBig
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))
-> r)
-> ValidSize
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))
-> (forall r.
TooBig
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))
-> r)
-> ValidSize
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))
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
forall r.
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 = Sing
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))
-> (forall r.
TooBig
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))
-> r)
-> ValidSize
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
TooBig
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))
-> r)
-> ValidSize
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))
-> (forall r.
TooBig
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))
-> r)
-> ValidSize
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))
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
forall r.
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 = Sing
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))
-> (forall r.
TooBig
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))
-> r)
-> ValidSize
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
TooBig
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))
-> r)
-> ValidSize
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))
-> (forall r.
TooBig
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))
-> r)
-> ValidSize
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))
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
forall r.
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 = Sing
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))
-> (forall r.
TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))
-> r)
-> ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))
-> r)
-> ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))
-> (forall r.
TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))
-> r)
-> ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))
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
forall r.
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 = Sing
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))
-> (forall r.
TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))
-> r)
-> ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))
-> r)
-> ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))
-> (forall r.
TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))
-> r)
-> ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))
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
forall r.
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 = Sing
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))
-> (forall r.
TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))
-> r)
-> ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))
-> r)
-> ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))
-> (forall r.
TooBig
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))
-> r)
-> ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))
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
forall r.
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 = Sing
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))
-> (forall r.
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)
-> ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S 'Z))))))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
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)
-> ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S 'Z)))))))))))))))))))))))
-> (forall r.
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)
-> ValidSize
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S ('S 'Z))))))))))))))))))))))
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
forall r.
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 = Sing
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S 'Z)))))))))))))))))))))))
-> (forall r.
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)
-> 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)))))))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S ('S ('S ('S 'Z)))))))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
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)
-> 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))))))))))))))))))))))))
-> (forall r.
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)
-> 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)))))))))))))))))))))))
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
forall r.
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 = Sing
('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))))))))))))))))))))))))
-> (forall r.
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)
-> 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))))))))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
('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))))))))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
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)
-> 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)))))))))))))))))))))))))
-> (forall r.
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)
-> 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))))))))))))))))))))))))
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
forall r.
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 = Sing
('S
('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)))))))))))))))))))))))))
-> (forall r.
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)
-> 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)))))))))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
('S
('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)))))))))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
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)
-> 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))))))))))))))))))))))))))
-> (forall r.
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)
-> 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)))))))))))))))))))))))))
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
forall r.
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 = Sing
('S
('S
('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))))))))))))))))))))))))))
-> (forall r.
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)
-> 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))))))))))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
('S
('S
('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))))))))))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
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)
-> 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)))))))))))))))))))))))))))
-> (forall r.
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)
-> 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))))))))))))))))))))))))))
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
forall r.
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 = Sing
('S
('S
('S
('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)))))))))))))))))))))))))))
-> (forall r.
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)
-> 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)))))))))))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
('S
('S
('S
('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)))))))))))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
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)
-> 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))))))))))))))))))))))))))))
-> (forall r.
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)
-> 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)))))))))))))))))))))))))))
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
forall r.
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 = Sing
('S
('S
('S
('S
('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))))))))))))))))))))))))))))
-> (forall r.
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)
-> 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))))))))))))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
('S
('S
('S
('S
('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))))))))))))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
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)
-> 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)))))))))))))))))))))))))))))
-> (forall r.
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)
-> 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))))))))))))))))))))))))))))
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
forall r.
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 = Sing
('S
('S
('S
('S
('S
('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)))))))))))))))))))))))))))))
-> (forall r.
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)
-> 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)))))))))))))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
('S
('S
('S
('S
('S
('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)))))))))))))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
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)
-> 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))))))))))))))))))))))))))))))
-> (forall r.
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)
-> 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)))))))))))))))))))))))))))))
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
forall r.
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 = Sing
('S
('S
('S
('S
('S
('S
('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))))))))))))))))))))))))))))))
-> (forall r.
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)
-> 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))))))))))))))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
('S
('S
('S
('S
('S
('S
('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))))))))))))))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
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)
-> 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)))))))))))))))))))))))))))))))
-> (forall r.
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)
-> 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))))))))))))))))))))))))))))))
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
forall r.
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 = Sing
('S
('S
('S
('S
('S
('S
('S
('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)))))))))))))))))))))))))))))))
-> (forall r.
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)
-> 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)))))))))))))))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
('S
('S
('S
('S
('S
('S
('S
('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)))))))))))))))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
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)
-> 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))))))))))))))))))))))))))))))))
-> (forall r.
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)
-> 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)))))))))))))))))))))))))))))))
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
forall r.
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 = Sing
('S
('S
('S
('S
('S
('S
('S
('S
('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))))))))))))))))))))))))))))))))
-> (forall r.
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)
-> 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))))))))))))))))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
('S
('S
('S
('S
('S
('S
('S
('S
('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))))))))))))))))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
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)
-> 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)))))))))))))))))))))))))))))))))
-> (forall r.
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)
-> 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))))))))))))))))))))))))))))))))
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
forall r.
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 = Sing
('S
('S
('S
('S
('S
('S
('S
('S
('S
('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)))))))))))))))))))))))))))))))))
-> (forall r.
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)
-> 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)))))))))))))))))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
('S
('S
('S
('S
('S
('S
('S
('S
('S
('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)))))))))))))))))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
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)
-> 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))))))))))))))))))))))))))))))))))
-> (forall r.
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)
-> 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)))))))))))))))))))))))))))))))))
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
forall r.
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 = Sing
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('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))))))))))))))))))))))))))))))))))
-> (forall r.
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)
-> 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))))))))))))))))))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('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))))))))))))))))))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
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)
-> 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)))))))))))))))))))))))))))))))))))
-> (forall r.
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)
-> 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))))))))))))))))))))))))))))))))))
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
forall r.
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 = Sing
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('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)))))))))))))))))))))))))))))))))))
-> (forall r.
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)
-> 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)))))))))))))))))))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('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)))))))))))))))))))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
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)
-> 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))))))))))))))))))))))))))))))))))))
-> (forall r.
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)
-> 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)))))))))))))))))))))))))))))))))))
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
forall r.
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 = Sing
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('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))))))))))))))))))))))))))))))))))))
-> (forall r.
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)
-> 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))))))))))))))))))))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('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))))))))))))))))))))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
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)
-> 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)))))))))))))))))))))))))))))))))))))
-> (forall r.
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)
-> 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))))))))))))))))))))))))))))))))))))
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
forall r.
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 = Sing
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('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)))))))))))))))))))))))))))))))))))))
-> (forall r.
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)
-> 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)))))))))))))))))))))))))))))))))))))
forall (n :: Nat).
Sing n -> (forall r. TooBig n -> r) -> ValidSize n
ValidSize Sing
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('S
('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)))))))))))))))))))))))))))))))))))))
forall k (a :: k). SingI a => Sing a
sing ((forall r.
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)
-> 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))))))))))))))))))))))))))))))))))))))
-> (forall r.
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)
-> ValidSize
('S
('S
('S
('S
('S
('S
('S
('S