{-# LANGUAGE Trustworthy, TypeFamilies, TypeOperators #-}
{-# LANGUAGE UndecidableInstances, FlexibleInstances #-}
module SDP.Finite
(
E (..), (:&) (..),
I1, I2, I3, I4, I5, I6, I7, I8, I9, I10, I11, I12, I13, I14, I15,
ind2, ind3, ind4, ind5, ind6, ind7, ind8, ind9,
ind10, ind11, ind12, ind13, ind14, ind15
)
where
import Prelude ( (++) )
import SDP.SafePrelude
import SDP.Nullable
import Data.Default.Class
import GHC.Types
import GHC.Read
import qualified GHC.Exts as E
import GHC.Exts ( IsList )
import Control.Exception.SDP
default ()
data E = E deriving ( E -> E -> Bool
(E -> E -> Bool) -> (E -> E -> Bool) -> Eq E
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: E -> E -> Bool
$c/= :: E -> E -> Bool
== :: E -> E -> Bool
$c== :: E -> E -> Bool
Eq, Eq E
Eq E
-> (E -> E -> Ordering)
-> (E -> E -> Bool)
-> (E -> E -> Bool)
-> (E -> E -> Bool)
-> (E -> E -> Bool)
-> (E -> E -> E)
-> (E -> E -> E)
-> Ord E
E -> E -> Bool
E -> E -> Ordering
E -> E -> E
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: E -> E -> E
$cmin :: E -> E -> E
max :: E -> E -> E
$cmax :: E -> E -> E
>= :: E -> E -> Bool
$c>= :: E -> E -> Bool
> :: E -> E -> Bool
$c> :: E -> E -> Bool
<= :: E -> E -> Bool
$c<= :: E -> E -> Bool
< :: E -> E -> Bool
$c< :: E -> E -> Bool
compare :: E -> E -> Ordering
$ccompare :: E -> E -> Ordering
$cp1Ord :: Eq E
Ord, Int -> E -> ShowS
[E] -> ShowS
E -> String
(Int -> E -> ShowS) -> (E -> String) -> ([E] -> ShowS) -> Show E
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [E] -> ShowS
$cshowList :: [E] -> ShowS
show :: E -> String
$cshow :: E -> String
showsPrec :: Int -> E -> ShowS
$cshowsPrec :: Int -> E -> ShowS
Show, ReadPrec [E]
ReadPrec E
Int -> ReadS E
ReadS [E]
(Int -> ReadS E)
-> ReadS [E] -> ReadPrec E -> ReadPrec [E] -> Read E
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [E]
$creadListPrec :: ReadPrec [E]
readPrec :: ReadPrec E
$creadPrec :: ReadPrec E
readList :: ReadS [E]
$creadList :: ReadS [E]
readsPrec :: Int -> ReadS E
$creadsPrec :: Int -> ReadS E
Read )
instance Default E where def :: E
def = E
E
instance IsList E
where
type Item E = E
fromList :: [Item E] -> E
fromList = E -> [E] -> E
forall a b. a -> b -> a
const E
E
toList :: E -> [Item E]
toList = [E] -> E -> [E]
forall a b. a -> b -> a
const []
instance Nullable E where lzero :: E
lzero = E
E; isNull :: E -> Bool
isNull = Bool -> E -> Bool
forall a b. a -> b -> a
const Bool
True
data tail :& head = !tail :& !head deriving ( (tail :& head) -> (tail :& head) -> Bool
((tail :& head) -> (tail :& head) -> Bool)
-> ((tail :& head) -> (tail :& head) -> Bool) -> Eq (tail :& head)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall tail head.
(Eq tail, Eq head) =>
(tail :& head) -> (tail :& head) -> Bool
/= :: (tail :& head) -> (tail :& head) -> Bool
$c/= :: forall tail head.
(Eq tail, Eq head) =>
(tail :& head) -> (tail :& head) -> Bool
== :: (tail :& head) -> (tail :& head) -> Bool
$c== :: forall tail head.
(Eq tail, Eq head) =>
(tail :& head) -> (tail :& head) -> Bool
Eq, Eq (tail :& head)
Eq (tail :& head)
-> ((tail :& head) -> (tail :& head) -> Ordering)
-> ((tail :& head) -> (tail :& head) -> Bool)
-> ((tail :& head) -> (tail :& head) -> Bool)
-> ((tail :& head) -> (tail :& head) -> Bool)
-> ((tail :& head) -> (tail :& head) -> Bool)
-> ((tail :& head) -> (tail :& head) -> tail :& head)
-> ((tail :& head) -> (tail :& head) -> tail :& head)
-> Ord (tail :& head)
(tail :& head) -> (tail :& head) -> Bool
(tail :& head) -> (tail :& head) -> Ordering
(tail :& head) -> (tail :& head) -> tail :& head
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall tail head. (Ord tail, Ord head) => Eq (tail :& head)
forall tail head.
(Ord tail, Ord head) =>
(tail :& head) -> (tail :& head) -> Bool
forall tail head.
(Ord tail, Ord head) =>
(tail :& head) -> (tail :& head) -> Ordering
forall tail head.
(Ord tail, Ord head) =>
(tail :& head) -> (tail :& head) -> tail :& head
min :: (tail :& head) -> (tail :& head) -> tail :& head
$cmin :: forall tail head.
(Ord tail, Ord head) =>
(tail :& head) -> (tail :& head) -> tail :& head
max :: (tail :& head) -> (tail :& head) -> tail :& head
$cmax :: forall tail head.
(Ord tail, Ord head) =>
(tail :& head) -> (tail :& head) -> tail :& head
>= :: (tail :& head) -> (tail :& head) -> Bool
$c>= :: forall tail head.
(Ord tail, Ord head) =>
(tail :& head) -> (tail :& head) -> Bool
> :: (tail :& head) -> (tail :& head) -> Bool
$c> :: forall tail head.
(Ord tail, Ord head) =>
(tail :& head) -> (tail :& head) -> Bool
<= :: (tail :& head) -> (tail :& head) -> Bool
$c<= :: forall tail head.
(Ord tail, Ord head) =>
(tail :& head) -> (tail :& head) -> Bool
< :: (tail :& head) -> (tail :& head) -> Bool
$c< :: forall tail head.
(Ord tail, Ord head) =>
(tail :& head) -> (tail :& head) -> Bool
compare :: (tail :& head) -> (tail :& head) -> Ordering
$ccompare :: forall tail head.
(Ord tail, Ord head) =>
(tail :& head) -> (tail :& head) -> Ordering
$cp1Ord :: forall tail head. (Ord tail, Ord head) => Eq (tail :& head)
Ord )
instance (Enum i) => Enum (E :& i)
where
fromEnum :: (E :& i) -> Int
fromEnum (E
E :& i
e) = i -> Int
forall a. Enum a => a -> Int
fromEnum i
e
succ :: (E :& i) -> E :& i
succ (E
E :& i
e) = E
E E -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:& i -> i
forall a. Enum a => a -> a
succ i
e
pred :: (E :& i) -> E :& i
pred (E
E :& i
e) = E
E E -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:& i -> i
forall a. Enum a => a -> a
pred i
e
toEnum :: Int -> E :& i
toEnum = (E
E E -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&) (i -> E :& i) -> (Int -> i) -> Int -> E :& i
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Int -> i
forall a. Enum a => Int -> a
toEnum
enumFrom :: (E :& i) -> [E :& i]
enumFrom (E
E :& i
f) = (E
E E -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&) (i -> E :& i) -> [i] -> [E :& i]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [i
f ..]
enumFromTo :: (E :& i) -> (E :& i) -> [E :& i]
enumFromTo (E
E :& i
f) (E
E :& i
l) = (E
E E -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&) (i -> E :& i) -> [i] -> [E :& i]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [i
f .. i
l]
enumFromThen :: (E :& i) -> (E :& i) -> [E :& i]
enumFromThen (E
E :& i
f) (E
E :& i
n) = (E
E E -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&) (i -> E :& i) -> [i] -> [E :& i]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [i
f, i
n ..]
enumFromThenTo :: (E :& i) -> (E :& i) -> (E :& i) -> [E :& i]
enumFromThenTo (E
E :& i
f) (E
E :& i
n) (E
E :& i
l) = (E
E E -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&) (i -> E :& i) -> [i] -> [E :& i]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [i
f, i
n .. i
l]
instance (Default d, Default d') => Default (d :& d') where def :: d :& d'
def = d
forall a. Default a => a
def d -> d' -> d :& d'
forall tail head. tail -> head -> tail :& head
:& d'
forall a. Default a => a
def
instance (IsList (i' :& i), E.Item (i' :& i) ~~ i, Show i) => Show (i' :& i)
where
showsPrec :: Int -> (i' :& i) -> ShowS
showsPrec Int
p = Int -> [Item (i' :& i)] -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p ([Item (i' :& i)] -> ShowS)
-> ((i' :& i) -> [Item (i' :& i)]) -> (i' :& i) -> ShowS
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (i' :& i) -> [Item (i' :& i)]
forall l. IsList l => l -> [Item l]
E.toList
instance (IsList (i' :& i), E.Item (i' :& i) ~~ i, Read i) => Read (i' :& i)
where
readPrec :: ReadPrec (i' :& i)
readPrec = [i] -> i' :& i
forall l. IsList l => [Item l] -> l
E.fromList ([i] -> i' :& i) -> ReadPrec [i] -> ReadPrec (i' :& i)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReadPrec [i]
forall a. Read a => ReadPrec a
readPrec
instance IsList (E :& i)
where
type Item (E :& i) = i
fromList :: [Item (E :& i)] -> E :& i
fromList [Item (E :& i)
i] = E
E E -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:& i
Item (E :& i)
i
fromList [Item (E :& i)]
_ = IndexException -> E :& i
forall a e. Exception e => e -> a
throw (IndexException -> E :& i) -> IndexException -> E :& i
forall a b. (a -> b) -> a -> b
$ String -> IndexException
UnexpectedRank String
"in SDP.Finite.fromList"
toList :: (E :& i) -> [Item (E :& i)]
toList (E
E :& i
i) = [i
Item (E :& i)
i]
instance (E.Item (i' :& i) ~~ i, IsList (i' :& i)) => IsList (i' :& i :& i)
where
type Item (i' :& i :& i) = i
toList :: ((i' :& i) :& i) -> [Item ((i' :& i) :& i)]
toList (i' :& i
i' :& i
i) = (i' :& i) -> [Item (i' :& i)]
forall l. IsList l => l -> [Item l]
E.toList i' :& i
i' [i] -> [i] -> [i]
forall a. [a] -> [a] -> [a]
++ [i
i]
fromList :: [Item ((i' :& i) :& i)] -> (i' :& i) :& i
fromList = (([Item (i' :& i)] -> i -> (i' :& i) :& i)
-> ([Item (i' :& i)], i) -> (i' :& i) :& i
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (([Item (i' :& i)] -> i -> (i' :& i) :& i)
-> ([Item (i' :& i)], i) -> (i' :& i) :& i)
-> ([Item (i' :& i)] -> i -> (i' :& i) :& i)
-> ([Item (i' :& i)], i)
-> (i' :& i) :& i
forall a b. (a -> b) -> a -> b
$ (i' :& i) -> i -> (i' :& i) :& i
forall tail head. tail -> head -> tail :& head
(:&) ((i' :& i) -> i -> (i' :& i) :& i)
-> ([Item (i' :& i)] -> i' :& i)
-> [Item (i' :& i)]
-> i
-> (i' :& i) :& i
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. [Item (i' :& i)] -> i' :& i
forall l. IsList l => [Item l] -> l
E.fromList) (([Item (i' :& i)], i) -> (i' :& i) :& i)
-> ([i] -> ([Item (i' :& i)], i)) -> [i] -> (i' :& i) :& i
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. [i] -> ([Item (i' :& i)], i)
forall i. [i] -> ([i], i)
unsnoc
type I1 i = E :& i
type I2 i = E :& i :& i
type I3 i = (I2 i) :& i
type I4 i = (I3 i) :& i
type I5 i = (I4 i) :& i
type I6 i = (I5 i) :& i
type I7 i = (I6 i) :& i
type I8 i = (I7 i) :& i
type I9 i = (I8 i) :& i
type I10 i = (I9 i) :& i
type I11 i = (I10 i) :& i
type I12 i = (I11 i) :& i
type I13 i = (I12 i) :& i
type I14 i = (I13 i) :& i
type I15 i = (I14 i) :& i
ind2 :: i -> i -> I2 i
ind3 :: i -> i -> i -> I3 i
ind4 :: i -> i -> i -> i -> I4 i
ind5 :: i -> i -> i -> i -> i -> I5 i
ind6 :: i -> i -> i -> i -> i -> i -> I6 i
ind7 :: i -> i -> i -> i -> i -> i -> i -> I7 i
ind8 :: i -> i -> i -> i -> i -> i -> i -> i -> I8 i
ind9 :: i -> i -> i -> i -> i -> i -> i -> i -> i -> I9 i
ind10 :: i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> I10 i
ind11 :: i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> I11 i
ind12 :: i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> I12 i
ind13 :: i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> I13 i
ind14 :: i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> I14 i
ind15 :: i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> I15 i
ind2 :: i -> i -> I2 i
ind2 i
a i
b = E
EE -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&i
a(E :& i) -> i -> I2 i
forall tail head. tail -> head -> tail :& head
:&i
b
ind3 :: i -> i -> i -> I3 i
ind3 i
a i
b i
c = E
EE -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&i
a(E :& i) -> i -> (E :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
b((E :& i) :& i) -> i -> I3 i
forall tail head. tail -> head -> tail :& head
:&i
c
ind4 :: i -> i -> i -> i -> I4 i
ind4 i
a i
b i
c i
d = E
EE -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&i
a(E :& i) -> i -> (E :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
b((E :& i) :& i) -> i -> ((E :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
c(((E :& i) :& i) :& i) -> i -> I4 i
forall tail head. tail -> head -> tail :& head
:&i
d
ind5 :: i -> i -> i -> i -> i -> I5 i
ind5 i
a i
b i
c i
d i
e = E
EE -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&i
a(E :& i) -> i -> (E :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
b((E :& i) :& i) -> i -> ((E :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
c(((E :& i) :& i) :& i) -> i -> (((E :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
d((((E :& i) :& i) :& i) :& i) -> i -> I5 i
forall tail head. tail -> head -> tail :& head
:&i
e
ind6 :: i -> i -> i -> i -> i -> i -> I6 i
ind6 i
a i
b i
c i
d i
e i
f = E
EE -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&i
a(E :& i) -> i -> (E :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
b((E :& i) :& i) -> i -> ((E :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
c(((E :& i) :& i) :& i) -> i -> (((E :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
d((((E :& i) :& i) :& i) :& i)
-> i -> ((((E :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
e(((((E :& i) :& i) :& i) :& i) :& i) -> i -> I6 i
forall tail head. tail -> head -> tail :& head
:&i
f
ind7 :: i -> i -> i -> i -> i -> i -> i -> I7 i
ind7 i
a i
b i
c i
d i
e i
f i
g = E
EE -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&i
a(E :& i) -> i -> (E :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
b((E :& i) :& i) -> i -> ((E :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
c(((E :& i) :& i) :& i) -> i -> (((E :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
d((((E :& i) :& i) :& i) :& i)
-> i -> ((((E :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
e(((((E :& i) :& i) :& i) :& i) :& i)
-> i -> (((((E :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
f((((((E :& i) :& i) :& i) :& i) :& i) :& i) -> i -> I7 i
forall tail head. tail -> head -> tail :& head
:&i
g
ind8 :: i -> i -> i -> i -> i -> i -> i -> i -> I8 i
ind8 i
a i
b i
c i
d i
e i
f i
g i
h = E
EE -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&i
a(E :& i) -> i -> (E :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
b((E :& i) :& i) -> i -> ((E :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
c(((E :& i) :& i) :& i) -> i -> (((E :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
d((((E :& i) :& i) :& i) :& i)
-> i -> ((((E :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
e(((((E :& i) :& i) :& i) :& i) :& i)
-> i -> (((((E :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
f((((((E :& i) :& i) :& i) :& i) :& i) :& i)
-> i -> ((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
g(((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) -> i -> I8 i
forall tail head. tail -> head -> tail :& head
:&i
h
ind9 :: i -> i -> i -> i -> i -> i -> i -> i -> i -> I9 i
ind9 i
a i
b i
c i
d i
e i
f i
g i
h i
i = E
EE -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&i
a(E :& i) -> i -> (E :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
b((E :& i) :& i) -> i -> ((E :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
c(((E :& i) :& i) :& i) -> i -> (((E :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
d((((E :& i) :& i) :& i) :& i)
-> i -> ((((E :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
e(((((E :& i) :& i) :& i) :& i) :& i)
-> i -> (((((E :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
f((((((E :& i) :& i) :& i) :& i) :& i) :& i)
-> i -> ((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
g(((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i -> (((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
h((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i -> I9 i
forall tail head. tail -> head -> tail :& head
:&i
i
ind10 :: i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> I10 i
ind10 i
a i
b i
c i
d i
e i
f i
g i
h i
i i
j = E
EE -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&i
a(E :& i) -> i -> (E :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
b((E :& i) :& i) -> i -> ((E :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
c(((E :& i) :& i) :& i) -> i -> (((E :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
d((((E :& i) :& i) :& i) :& i)
-> i -> ((((E :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
e(((((E :& i) :& i) :& i) :& i) :& i)
-> i -> (((((E :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
f((((((E :& i) :& i) :& i) :& i) :& i) :& i)
-> i -> ((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
g(((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i -> (((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
h((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i
-> ((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
i(((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i -> I10 i
forall tail head. tail -> head -> tail :& head
:&i
j
ind11 :: i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> I11 i
ind11 i
a i
b i
c i
d i
e i
f i
g i
h i
i i
j i
k = E
EE -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&i
a(E :& i) -> i -> (E :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
b((E :& i) :& i) -> i -> ((E :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
c(((E :& i) :& i) :& i) -> i -> (((E :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
d((((E :& i) :& i) :& i) :& i)
-> i -> ((((E :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
e(((((E :& i) :& i) :& i) :& i) :& i)
-> i -> (((((E :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
f((((((E :& i) :& i) :& i) :& i) :& i) :& i)
-> i -> ((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
g(((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i -> (((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
h((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i
-> ((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
i(((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i
-> (((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
:& i
forall tail head. tail -> head -> tail :& head
:&i
j((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
:& i)
-> i -> I11 i
forall tail head. tail -> head -> tail :& head
:&i
k
ind12 :: i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> i -> I12 i
ind12 i
a i
b i
c i
d i
e i
f i
g i
h i
i i
j i
k i
l = E
EE -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&i
a(E :& i) -> i -> (E :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
b((E :& i) :& i) -> i -> ((E :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
c(((E :& i) :& i) :& i) -> i -> (((E :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
d((((E :& i) :& i) :& i) :& i)
-> i -> ((((E :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
e(((((E :& i) :& i) :& i) :& i) :& i)
-> i -> (((((E :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
f((((((E :& i) :& i) :& i) :& i) :& i) :& i)
-> i -> ((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
g(((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i -> (((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
h((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i
-> ((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
i(((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i
-> (((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
:& i
forall tail head. tail -> head -> tail :& head
:&i
j((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
:& i)
-> i
-> ((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
:& i)
:& i)
:& i
forall tail head. tail -> head -> tail :& head
:&i
k(((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
:& i)
:& i)
-> i -> I12 i
forall tail head. tail -> head -> tail :& head
:&i
l
ind13 :: i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> I13 i
ind13 i
a i
b i
c i
d i
e i
f i
g i
h i
i i
j i
k i
l i
m = E
EE -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&i
a(E :& i) -> i -> (E :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
b((E :& i) :& i) -> i -> ((E :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
c(((E :& i) :& i) :& i) -> i -> (((E :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
d((((E :& i) :& i) :& i) :& i)
-> i -> ((((E :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
e(((((E :& i) :& i) :& i) :& i) :& i)
-> i -> (((((E :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
f((((((E :& i) :& i) :& i) :& i) :& i) :& i)
-> i -> ((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
g(((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i -> (((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
h((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i
-> ((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
i(((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i
-> (((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
:& i
forall tail head. tail -> head -> tail :& head
:&i
j((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
:& i)
-> i
-> ((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
:& i)
:& i)
:& i
forall tail head. tail -> head -> tail :& head
:&i
k(((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
:& i)
:& i)
-> i
-> (((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
:& i)
:& i)
:& i)
:& i
forall tail head. tail -> head -> tail :& head
:&i
l((((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
:& i)
:& i)
:& i)
-> i -> I13 i
forall tail head. tail -> head -> tail :& head
:&i
m
ind14 :: i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> I14 i
ind14 i
a i
b i
c i
d i
e i
f i
g i
h i
i i
j i
k i
l i
m i
n = E
EE -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&i
a(E :& i) -> i -> (E :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
b((E :& i) :& i) -> i -> ((E :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
c(((E :& i) :& i) :& i) -> i -> (((E :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
d((((E :& i) :& i) :& i) :& i)
-> i -> ((((E :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
e(((((E :& i) :& i) :& i) :& i) :& i)
-> i -> (((((E :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
f((((((E :& i) :& i) :& i) :& i) :& i) :& i)
-> i -> ((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
g(((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i -> (((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
h((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i
-> ((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
i(((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i
-> (((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
:& i
forall tail head. tail -> head -> tail :& head
:&i
j((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
:& i)
-> i
-> ((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
:& i)
:& i)
:& i
forall tail head. tail -> head -> tail :& head
:&i
k(((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
:& i)
:& i)
-> i
-> (((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
:& i)
:& i)
:& i)
:& i
forall tail head. tail -> head -> tail :& head
:&i
l((((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
:& i)
:& i)
:& i)
-> i
-> ((((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
:& i)
:& i)
:& i)
:& i)
:& i
forall tail head. tail -> head -> tail :& head
:&i
m(((((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
:& i)
:& i)
:& i)
:& i)
:& i)
-> i -> I14 i
forall tail head. tail -> head -> tail :& head
:&i
n
ind15 :: i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> i
-> I15 i
ind15 i
a i
b i
c i
d i
e i
f i
g i
h i
i i
j i
k i
l i
m i
n i
o = E
EE -> i -> E :& i
forall tail head. tail -> head -> tail :& head
:&i
a(E :& i) -> i -> (E :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
b((E :& i) :& i) -> i -> ((E :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
c(((E :& i) :& i) :& i) -> i -> (((E :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
d((((E :& i) :& i) :& i) :& i)
-> i -> ((((E :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
e(((((E :& i) :& i) :& i) :& i) :& i)
-> i -> (((((E :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
f((((((E :& i) :& i) :& i) :& i) :& i) :& i)
-> i -> ((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
g(((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i -> (((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
h((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i
-> ((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i
forall tail head. tail -> head -> tail :& head
:&i
i(((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
-> i
-> (((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
:& i
forall tail head. tail -> head -> tail :& head
:&i
j((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
:& i)
-> i
-> ((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
:& i)
:& i)
:& i
forall tail head. tail -> head -> tail :& head
:&i
k(((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
:& i)
:& i)
-> i
-> (((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
:& i)
:& i)
:& i)
:& i
forall tail head. tail -> head -> tail :& head
:&i
l((((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
:& i)
:& i)
:& i)
-> i
-> ((((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
:& i)
:& i)
:& i)
:& i)
:& i
forall tail head. tail -> head -> tail :& head
:&i
m(((((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
:& i)
:& i)
:& i)
:& i)
:& i)
-> i
-> (((((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
:& i)
:& i)
:& i)
:& i)
:& i)
:& i
forall tail head. tail -> head -> tail :& head
:&i
n((((((((((((((E :& i) :& i) :& i) :& i) :& i) :& i) :& i) :& i)
:& i)
:& i)
:& i)
:& i)
:& i)
:& i)
-> i -> I15 i
forall tail head. tail -> head -> tail :& head
:&i
o
unsnoc :: [i] -> ([i], i)
unsnoc :: [i] -> ([i], i)
unsnoc [i
i] = ([], i
i)
unsnoc (i
i : [i]
is) = (i
i i -> [i] -> [i]
forall a. a -> [a] -> [a]
:) ([i] -> [i]) -> ([i], i) -> ([i], i)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
`first` [i] -> ([i], i)
forall i. [i] -> ([i], i)
unsnoc [i]
is
unsnoc [i]
_ = IndexException -> ([i], i)
forall a e. Exception e => e -> a
throw (IndexException -> ([i], i)) -> IndexException -> ([i], i)
forall a b. (a -> b) -> a -> b
$ String -> IndexException
UnexpectedRank String
"in SDP.Finite.fromList"