{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE IncoherentInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE StandaloneDeriving #-}
#if __GLASGOW_HASKELL__ < 806
{-# LANGUAGE TypeInType #-}
#endif
{-# OPTIONS_HADDOCK hide #-}
module Data.Parameterized.Context.Safe
( module Data.Parameterized.Ctx
, Size
, sizeInt
, zeroSize
, incSize
, decSize
, extSize
, addSize
, SizeView(..)
, viewSize
, sizeToNatRepr
, KnownContext(..)
, Diff
, noDiff
, addDiff
, extendRight
, appendDiff
, DiffView(..)
, viewDiff
, KnownDiff(..)
, IsAppend(..)
, diffIsAppend
, Index
, indexVal
, baseIndex
, skipIndex
, lastIndex
, nextIndex
, leftIndex
, rightIndex
, extendIndex
, extendIndex'
, extendIndexAppendLeft
, forIndex
, forIndexRange
, intIndex
, IndexView(..)
, viewIndex
, Assignment
, size
, Data.Parameterized.Context.Safe.replicate
, generate
, generateM
, empty
, extend
, adjust
, update
, adjustM
, AssignView(..)
, viewAssign
, (!)
, (!^)
, zipWith
, zipWithM
, (<++>)
, traverseWithIndex
) where
import qualified Control.Category as Cat
import Control.DeepSeq
import qualified Control.Lens as Lens
import Control.Monad.Identity (Identity(..))
import Data.Hashable
import Data.List (intercalate)
import Data.Maybe (listToMaybe)
import Data.Type.Equality
import Prelude hiding (init, map, null, replicate, succ, zipWith)
import Data.Kind(Type)
import Data.Parameterized.Classes
import Data.Parameterized.Ctx
import Data.Parameterized.NatRepr
import Data.Parameterized.Some
import Data.Parameterized.TraversableFC
import Data.Parameterized.TraversableFC.WithIndex
data Size (ctx :: Ctx k) where
SizeZero :: Size 'EmptyCtx
SizeSucc :: !(Size ctx) -> Size (ctx '::> tp)
instance Show (Size ctx) where
show :: Size ctx -> String
show = Int -> String
forall a. Show a => a -> String
show (Int -> String) -> (Size ctx -> Int) -> Size ctx -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Size ctx -> Int
forall {k} (ctx :: Ctx k). Size ctx -> Int
sizeInt
instance ShowF Size
sizeInt :: Size ctx -> Int
sizeInt :: forall {k} (ctx :: Ctx k). Size ctx -> Int
sizeInt Size ctx
SizeZero = Int
0
sizeInt (SizeSucc Size ctx
sz) = (Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (Int -> Int) -> Int -> Int
forall a b. (a -> b) -> a -> b
$! Size ctx -> Int
forall {k} (ctx :: Ctx k). Size ctx -> Int
sizeInt Size ctx
sz
zeroSize :: Size 'EmptyCtx
zeroSize :: forall {k}. Size 'EmptyCtx
zeroSize = Size 'EmptyCtx
forall {k}. Size 'EmptyCtx
SizeZero
incSize :: Size ctx -> Size (ctx '::> tp)
incSize :: forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
incSize Size ctx
sz = Size ctx -> Size (ctx '::> tp)
forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
SizeSucc Size ctx
sz
decSize :: Size (ctx '::> tp) -> Size ctx
decSize :: forall {k} (ctx :: Ctx k) (tp :: k). Size (ctx '::> tp) -> Size ctx
decSize (SizeSucc Size ctx
sz) = Size ctx
Size ctx
sz
addSize :: Size x -> Size y -> Size (x <+> y)
addSize :: forall {k} (x :: Ctx k) (y :: Ctx k).
Size x -> Size y -> Size (x <+> y)
addSize Size x
sx Size y
SizeZero = Size x
Size (x <+> y)
sx
addSize Size x
sx (SizeSucc Size ctx
sy) = Size (x <+> ctx) -> Size ((x <+> ctx) '::> tp)
forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
SizeSucc (Size x -> Size ctx -> Size (x <+> ctx)
forall {k} (x :: Ctx k) (y :: Ctx k).
Size x -> Size y -> Size (x <+> y)
addSize Size x
sx Size ctx
sy)
data SizeView (ctx :: Ctx k) where
ZeroSize :: SizeView 'EmptyCtx
IncSize :: !(Size ctx) -> SizeView (ctx '::> tp)
viewSize :: Size ctx -> SizeView ctx
viewSize :: forall {k} (ctx :: Ctx k). Size ctx -> SizeView ctx
viewSize Size ctx
SizeZero = SizeView ctx
SizeView 'EmptyCtx
forall {k}. SizeView 'EmptyCtx
ZeroSize
viewSize (SizeSucc Size ctx
s) = Size ctx -> SizeView (ctx '::> tp)
forall {k} (n :: Ctx k) (tp :: k). Size n -> SizeView (n '::> tp)
IncSize Size ctx
s
sizeToNatRepr :: Size items -> NatRepr (CtxSize items)
sizeToNatRepr :: forall {k} (items :: Ctx k). Size items -> NatRepr (CtxSize items)
sizeToNatRepr Size items
sz =
case Size items -> SizeView items
forall {k} (ctx :: Ctx k). Size ctx -> SizeView ctx
viewSize Size items
sz of
SizeView items
ZeroSize -> NatRepr 0
NatRepr (CtxSize items)
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
IncSize Size ctx
sz' ->
let oldRep :: NatRepr (CtxSize ctx)
oldRep = Size ctx -> NatRepr (CtxSize ctx)
forall {k} (items :: Ctx k). Size items -> NatRepr (CtxSize items)
sizeToNatRepr Size ctx
sz'
in case NatRepr 1
-> NatRepr (CtxSize ctx) -> (1 + CtxSize ctx) :~: (CtxSize ctx + 1)
forall (f :: Nat -> *) (m :: Nat) (g :: Nat -> *) (n :: Nat).
f m -> g n -> (m + n) :~: (n + m)
plusComm (NatRepr 1
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr :: NatRepr 1) NatRepr (CtxSize ctx)
oldRep of
(1 + CtxSize ctx) :~: (CtxSize ctx + 1)
Refl -> NatRepr (CtxSize ctx) -> NatRepr (CtxSize ctx + 1)
forall (n :: Nat). NatRepr n -> NatRepr (n + 1)
incNat NatRepr (CtxSize ctx)
oldRep
class KnownContext (ctx :: Ctx k) where
knownSize :: Size ctx
instance KnownContext 'EmptyCtx where
knownSize :: Size 'EmptyCtx
knownSize = Size 'EmptyCtx
forall {k}. Size 'EmptyCtx
zeroSize
instance KnownContext ctx => KnownContext (ctx '::> tp) where
knownSize :: Size (ctx '::> tp)
knownSize = Size ctx -> Size (ctx '::> tp)
forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
incSize Size ctx
forall k (ctx :: Ctx k). KnownContext ctx => Size ctx
knownSize
data Diff (l :: Ctx k) (r :: Ctx k) where
DiffHere :: Diff ctx ctx
DiffThere :: Diff ctx1 ctx2 -> Diff ctx1 (ctx2 '::> tp)
noDiff :: Diff l l
noDiff :: forall {k} (l :: Ctx k). Diff l l
noDiff = Diff l l
forall {k} (l :: Ctx k). Diff l l
DiffHere
addDiff :: Diff a b -> Diff b c -> Diff a c
addDiff :: forall {k} (a :: Ctx k) (b :: Ctx k) (c :: Ctx k).
Diff a b -> Diff b c -> Diff a c
addDiff Diff a b
x Diff b c
DiffHere = Diff a b
Diff a c
x
addDiff Diff a b
x (DiffThere Diff b ctx2
y) = Diff a ctx2 -> Diff a (ctx2 '::> tp)
forall {k} (ctx1 :: Ctx k) (n :: Ctx k) (tp :: k).
Diff ctx1 n -> Diff ctx1 (n '::> tp)
DiffThere (Diff a b -> Diff b ctx2 -> Diff a ctx2
forall {k} (a :: Ctx k) (b :: Ctx k) (c :: Ctx k).
Diff a b -> Diff b c -> Diff a c
addDiff Diff a b
x Diff b ctx2
y)
extendRight :: Diff l r -> Diff l (r '::> tp)
extendRight :: forall {k} (ctx1 :: Ctx k) (n :: Ctx k) (tp :: k).
Diff ctx1 n -> Diff ctx1 (n '::> tp)
extendRight Diff l r
diff = Diff l r -> Diff l (r '::> tp)
forall {k} (ctx1 :: Ctx k) (n :: Ctx k) (tp :: k).
Diff ctx1 n -> Diff ctx1 (n '::> tp)
DiffThere Diff l r
diff
appendDiff :: Size r -> Diff l (l <+> r)
appendDiff :: forall {k} (r :: Ctx k) (l :: Ctx k). Size r -> Diff l (l <+> r)
appendDiff Size r
SizeZero = Diff l l
Diff l (l <+> r)
forall {k} (l :: Ctx k). Diff l l
DiffHere
appendDiff (SizeSucc Size ctx
sz) = Diff l (l <+> ctx) -> Diff l ((l <+> ctx) '::> tp)
forall {k} (ctx1 :: Ctx k) (n :: Ctx k) (tp :: k).
Diff ctx1 n -> Diff ctx1 (n '::> tp)
DiffThere (Size ctx -> Diff l (l <+> ctx)
forall {k} (r :: Ctx k) (l :: Ctx k). Size r -> Diff l (l <+> r)
appendDiff Size ctx
sz)
instance Cat.Category Diff where
id :: forall (a :: Ctx k). Diff a a
id = Diff a a
forall {k} (l :: Ctx k). Diff l l
DiffHere
Diff b c
d1 . :: forall (b :: Ctx k) (c :: Ctx k) (a :: Ctx k).
Diff b c -> Diff a b -> Diff a c
. Diff a b
d2 = Diff a b -> Diff b c -> Diff a c
forall {k} (a :: Ctx k) (b :: Ctx k) (c :: Ctx k).
Diff a b -> Diff b c -> Diff a c
addDiff Diff a b
d2 Diff b c
d1
extSize :: Size l -> Diff l r -> Size r
extSize :: forall {k} (l :: Ctx k) (r :: Ctx k). Size l -> Diff l r -> Size r
extSize Size l
sz Diff l r
DiffHere = Size l
Size r
sz
extSize Size l
sz (DiffThere Diff l ctx2
diff) = Size ctx2 -> Size (ctx2 '::> tp)
forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
incSize (Size l -> Diff l ctx2 -> Size ctx2
forall {k} (l :: Ctx k) (r :: Ctx k). Size l -> Diff l r -> Size r
extSize Size l
sz Diff l ctx2
diff)
data IsAppend l r where
IsAppend :: Size app -> IsAppend l (l <+> app)
diffIsAppend :: Diff l r -> IsAppend l r
diffIsAppend :: forall {k} (l :: Ctx k) (r :: Ctx k). Diff l r -> IsAppend l r
diffIsAppend Diff l r
DiffHere = Size 'EmptyCtx -> IsAppend l (l <+> 'EmptyCtx)
forall {k} (n :: Ctx k) (l :: Ctx k).
Size n -> IsAppend l (l <+> n)
IsAppend Size 'EmptyCtx
forall {k}. Size 'EmptyCtx
zeroSize
diffIsAppend (DiffThere Diff l ctx2
diff) =
case Diff l ctx2 -> IsAppend l ctx2
forall {k} (l :: Ctx k) (r :: Ctx k). Diff l r -> IsAppend l r
diffIsAppend Diff l ctx2
diff of
IsAppend Size app
sz -> Size (app '::> tp) -> IsAppend l (l <+> (app '::> tp))
forall {k} (n :: Ctx k) (l :: Ctx k).
Size n -> IsAppend l (l <+> n)
IsAppend (Size app -> Size (app '::> tp)
forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
incSize Size app
sz)
data DiffView a b where
NoDiff :: DiffView a a
ExtendRightDiff :: Diff a b -> DiffView a (b ::> r)
viewDiff :: Diff a b -> DiffView a b
viewDiff :: forall {k} (a :: Ctx k) (b :: Ctx k). Diff a b -> DiffView a b
viewDiff Diff a b
DiffHere = DiffView a a
DiffView a b
forall {k} (a :: Ctx k). DiffView a a
NoDiff
viewDiff (DiffThere Diff a ctx2
diff) = Diff a ctx2 -> DiffView a (ctx2 '::> tp)
forall {k} (a :: Ctx k) (n :: Ctx k) (tp :: k).
Diff a n -> DiffView a (n ::> tp)
ExtendRightDiff Diff a ctx2
diff
class KnownDiff (l :: Ctx k) (r :: Ctx k) where
knownDiff :: Diff l r
instance KnownDiff l l where
knownDiff :: Diff l l
knownDiff = Diff l l
forall {k} (l :: Ctx k). Diff l l
noDiff
instance KnownDiff l r => KnownDiff l (r '::> tp) where
knownDiff :: Diff l (r '::> tp)
knownDiff = Diff l r -> Diff l (r '::> tp)
forall {k} (ctx1 :: Ctx k) (n :: Ctx k) (tp :: k).
Diff ctx1 n -> Diff ctx1 (n '::> tp)
extendRight Diff l r
forall k (l :: Ctx k) (r :: Ctx k). KnownDiff l r => Diff l r
knownDiff
data Index (ctx :: Ctx k) (tp :: k) where
IndexHere :: Size ctx -> Index (ctx '::> tp) tp
IndexThere :: !(Index ctx tp) -> Index (ctx '::> tp') tp
indexVal :: Index ctx tp -> Int
indexVal :: forall {k} (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
indexVal (IndexHere Size ctx
sz) = Size ctx -> Int
forall {k} (ctx :: Ctx k). Size ctx -> Int
sizeInt Size ctx
sz
indexVal (IndexThere Index ctx tp
idx) = Index ctx tp -> Int
forall {k} (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
indexVal Index ctx tp
idx
instance Eq (Index ctx tp) where
Index ctx tp
idx1 == :: Index ctx tp -> Index ctx tp -> Bool
== Index ctx tp
idx2 = Maybe (tp :~: tp) -> Bool
forall a. Maybe a -> Bool
isJust (Index ctx tp -> Index ctx tp -> Maybe (tp :~: tp)
forall (a :: k) (b :: k).
Index ctx a -> Index ctx b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Index ctx tp
idx1 Index ctx tp
idx2)
instance TestEquality (Index ctx) where
testEquality :: forall (a :: k) (b :: k).
Index ctx a -> Index ctx b -> Maybe (a :~: b)
testEquality (IndexHere Size ctx
_) (IndexHere Size ctx
_) = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
testEquality (IndexHere Size ctx
_) (IndexThere Index ctx b
_) = Maybe (a :~: b)
forall a. Maybe a
Nothing
testEquality (IndexThere Index ctx a
_) (IndexHere Size ctx
_) = Maybe (a :~: b)
forall a. Maybe a
Nothing
testEquality (IndexThere Index ctx a
idx1) (IndexThere Index ctx b
idx2) =
case Index ctx a -> Index ctx b -> Maybe (a :~: b)
forall (a :: k) (b :: k).
Index ctx a -> Index ctx b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Index ctx a
idx1 Index ctx b
Index ctx b
idx2 of
Just a :~: b
Refl -> (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
Maybe (a :~: b)
Nothing -> Maybe (a :~: b)
forall a. Maybe a
Nothing
instance Ord (Index ctx tp) where
compare :: Index ctx tp -> Index ctx tp -> Ordering
compare Index ctx tp
i Index ctx tp
j = OrderingF tp tp -> Ordering
forall {k} (x :: k) (y :: k). OrderingF x y -> Ordering
toOrdering (Index ctx tp -> Index ctx tp -> OrderingF tp tp
forall (x :: k) (y :: k).
Index ctx x -> Index ctx y -> OrderingF x y
forall k (ktp :: k -> *) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF Index ctx tp
i Index ctx tp
j)
instance OrdF (Index ctx) where
compareF :: forall (x :: k) (y :: k).
Index ctx x -> Index ctx y -> OrderingF x y
compareF (IndexHere Size ctx
_) (IndexHere Size ctx
_) = OrderingF x x
OrderingF x y
forall {k} (x :: k). OrderingF x x
EQF
compareF (IndexThere Index ctx x
_) (IndexHere Size ctx
_) = OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
LTF
compareF (IndexHere Size ctx
_) (IndexThere Index ctx y
_) = OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
GTF
compareF (IndexThere Index ctx x
idx1) (IndexThere Index ctx y
idx2) = Index ctx x
-> Index ctx y -> ((x ~ y) => OrderingF x y) -> OrderingF x y
forall j k (f :: j -> *) (a :: j) (b :: j) (c :: k) (d :: k).
OrdF f =>
f a -> f b -> ((a ~ b) => OrderingF c d) -> OrderingF c d
lexCompareF Index ctx x
idx1 Index ctx y
Index ctx y
idx2 (((x ~ y) => OrderingF x y) -> OrderingF x y)
-> ((x ~ y) => OrderingF x y) -> OrderingF x y
forall a b. (a -> b) -> a -> b
$ OrderingF x x
OrderingF x y
(x ~ y) => OrderingF x y
forall {k} (x :: k). OrderingF x x
EQF
baseIndex :: Index ('EmptyCtx '::> tp) tp
baseIndex :: forall {k} (tp :: k). Index ('EmptyCtx '::> tp) tp
baseIndex = Size 'EmptyCtx -> Index ('EmptyCtx '::> tp) tp
forall {k} (n :: Ctx k) (tp :: k). Size n -> Index (n '::> tp) tp
IndexHere Size 'EmptyCtx
forall {k}. Size 'EmptyCtx
SizeZero
skipIndex :: Index ctx x -> Index (ctx '::> y) x
skipIndex :: forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
skipIndex Index ctx x
idx = Index ctx x -> Index (ctx '::> y) x
forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
IndexThere Index ctx x
idx
nextIndex :: Size ctx -> Index (ctx '::> tp) tp
nextIndex :: forall {k} (n :: Ctx k) (tp :: k). Size n -> Index (n '::> tp) tp
nextIndex Size ctx
sz = Size ctx -> Index (ctx '::> tp) tp
forall {k} (n :: Ctx k) (tp :: k). Size n -> Index (n '::> tp) tp
IndexHere Size ctx
sz
lastIndex :: Size (ctx ::> tp) -> Index (ctx ::> tp) tp
lastIndex :: forall {k} (ctx :: Ctx k) (tp :: k).
Size (ctx ::> tp) -> Index (ctx ::> tp) tp
lastIndex (SizeSucc Size ctx
s) = Size ctx -> Index (ctx ::> tp) tp
forall {k} (n :: Ctx k) (tp :: k). Size n -> Index (n '::> tp) tp
IndexHere Size ctx
Size ctx
s
leftIndex :: Size r -> Index l tp -> Index (l <+> r) tp
leftIndex :: forall {k} (r :: Ctx k) (l :: Ctx k) (tp :: k).
Size r -> Index l tp -> Index (l <+> r) tp
leftIndex Size r
sr Index l tp
il = Diff l (l <+> r) -> Index l tp -> Index (l <+> r) tp
forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
Diff l r -> Index l tp -> Index r tp
extendIndex' (Size r -> Diff l (l <+> r)
forall {k} (r :: Ctx k) (l :: Ctx k). Size r -> Diff l (l <+> r)
appendDiff Size r
sr) Index l tp
il
rightIndex :: Size l -> Size r -> Index r tp -> Index (l <+> r) tp
rightIndex :: forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
Size l -> Size r -> Index r tp -> Index (l <+> r) tp
rightIndex Size l
sl Size r
sr Index r tp
ir =
case Size r -> Index r tp -> IndexView r tp
forall {k} (ctx :: Ctx k) (tp :: k).
Size ctx -> Index ctx tp -> IndexView ctx tp
viewIndex Size r
sr Index r tp
ir of
IndexViewInit Index ctx tp
i -> Index (l <+> ctx) tp -> Index ((l <+> ctx) '::> u) tp
forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
skipIndex (Size l -> Size ctx -> Index ctx tp -> Index (l <+> ctx) tp
forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
Size l -> Size r -> Index r tp -> Index (l <+> r) tp
rightIndex Size l
sl (Size (ctx '::> u) -> Size ctx
forall {k} (ctx :: Ctx k) (tp :: k). Size (ctx '::> tp) -> Size ctx
decSize Size r
Size (ctx '::> u)
sr) Index ctx tp
i)
IndexViewLast Size ctx
s -> Size ((l <+> ctx) ::> tp) -> Index ((l <+> ctx) ::> tp) tp
forall {k} (ctx :: Ctx k) (tp :: k).
Size (ctx ::> tp) -> Index (ctx ::> tp) tp
lastIndex (Size (l <+> ctx) -> Size ((l <+> ctx) ::> tp)
forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
incSize (Size l -> Size ctx -> Size (l <+> ctx)
forall {k} (x :: Ctx k) (y :: Ctx k).
Size x -> Size y -> Size (x <+> y)
addSize Size l
sl Size ctx
s))
{-# INLINE extendIndex #-}
extendIndex :: KnownDiff l r => Index l tp -> Index r tp
extendIndex :: forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
KnownDiff l r =>
Index l tp -> Index r tp
extendIndex = Diff l r -> Index l tp -> Index r tp
forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
Diff l r -> Index l tp -> Index r tp
extendIndex' Diff l r
forall k (l :: Ctx k) (r :: Ctx k). KnownDiff l r => Diff l r
knownDiff
{-# INLINE extendIndex' #-}
extendIndex' :: Diff l r -> Index l tp -> Index r tp
extendIndex' :: forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
Diff l r -> Index l tp -> Index r tp
extendIndex' Diff l r
DiffHere Index l tp
idx = Index l tp
Index r tp
idx
extendIndex' (DiffThere Diff l ctx2
diff) Index l tp
idx = Index ctx2 tp -> Index (ctx2 '::> tp) tp
forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
IndexThere (Diff l ctx2 -> Index l tp -> Index ctx2 tp
forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
Diff l r -> Index l tp -> Index r tp
extendIndex' Diff l ctx2
diff Index l tp
idx)
{-# INLINE extendIndexAppendLeft #-}
extendIndexAppendLeft :: Size l -> Size r -> Index r tp -> Index (l <+> r) tp
extendIndexAppendLeft :: forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
Size l -> Size r -> Index r tp -> Index (l <+> r) tp
extendIndexAppendLeft Size l
sz Size r
sz' Index r tp
idx = case Size r -> Index r tp -> IndexView r tp
forall {k} (ctx :: Ctx k) (tp :: k).
Size ctx -> Index ctx tp -> IndexView ctx tp
viewIndex Size r
sz' Index r tp
idx of
IndexViewLast Size ctx
_ -> Size ((l <+> ctx) ::> tp) -> Index ((l <+> ctx) ::> tp) tp
forall {k} (ctx :: Ctx k) (tp :: k).
Size (ctx ::> tp) -> Index (ctx ::> tp) tp
lastIndex (Size l -> Size r -> Size (l <+> r)
forall {k} (x :: Ctx k) (y :: Ctx k).
Size x -> Size y -> Size (x <+> y)
addSize Size l
sz Size r
sz')
IndexViewInit Index ctx tp
idx' -> Index (l <+> ctx) tp -> Index ((l <+> ctx) '::> u) tp
forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
skipIndex (Size l -> Size ctx -> Index ctx tp -> Index (l <+> ctx) tp
forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
Size l -> Size r -> Index r tp -> Index (l <+> r) tp
extendIndexAppendLeft Size l
sz (Size (ctx '::> u) -> Size ctx
forall {k} (ctx :: Ctx k) (tp :: k). Size (ctx '::> tp) -> Size ctx
decSize Size r
Size (ctx '::> u)
sz') Index ctx tp
idx')
forIndex :: forall ctx r
. Size ctx
-> (forall tp . r -> Index ctx tp -> r)
-> r
-> r
forIndex :: forall {k} (ctx :: Ctx k) r.
Size ctx -> (forall (tp :: k). r -> Index ctx tp -> r) -> r -> r
forIndex Size ctx
sz_top forall (tp :: k). r -> Index ctx tp -> r
f = (forall (tp :: k). Index ctx tp -> Index ctx tp)
-> Size ctx -> r -> r
forall (ctx' :: Ctx k).
(forall (tp :: k). Index ctx' tp -> Index ctx tp)
-> Size ctx' -> r -> r
go Index ctx tp -> Index ctx tp
forall (tp :: k). Index ctx tp -> Index ctx tp
forall a. a -> a
id Size ctx
sz_top
where go :: forall ctx'. (forall tp. Index ctx' tp -> Index ctx tp) -> Size ctx' -> r -> r
go :: forall (ctx' :: Ctx k).
(forall (tp :: k). Index ctx' tp -> Index ctx tp)
-> Size ctx' -> r -> r
go forall (tp :: k). Index ctx' tp -> Index ctx tp
_ Size ctx'
SizeZero = r -> r
forall a. a -> a
id
go forall (tp :: k). Index ctx' tp -> Index ctx tp
g (SizeSucc Size ctx
sz) = \r
r -> (forall (tp :: k). Index ctx tp -> Index ctx tp)
-> Size ctx -> r -> r
forall (ctx' :: Ctx k).
(forall (tp :: k). Index ctx' tp -> Index ctx tp)
-> Size ctx' -> r -> r
go (\Index ctx tp
i -> Index ctx' tp -> Index ctx tp
forall (tp :: k). Index ctx' tp -> Index ctx tp
g (Index ctx tp -> Index (ctx '::> tp) tp
forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
IndexThere Index ctx tp
i)) Size ctx
sz (r -> r) -> r -> r
forall a b. (a -> b) -> a -> b
$ r -> Index ctx tp -> r
forall (tp :: k). r -> Index ctx tp -> r
f r
r (Index ctx' tp -> Index ctx tp
forall (tp :: k). Index ctx' tp -> Index ctx tp
g (Size ctx -> Index (ctx '::> tp) tp
forall {k} (n :: Ctx k) (tp :: k). Size n -> Index (n '::> tp) tp
IndexHere Size ctx
sz))
data LDiff (l :: Ctx k) (r :: Ctx k) where
LDiffHere :: LDiff a a
LDiffThere :: !(LDiff (a::>x) b) -> LDiff a b
ldiffIndex :: Index a tp -> LDiff a b -> Index b tp
ldiffIndex :: forall {k} (a :: Ctx k) (tp :: k) (b :: Ctx k).
Index a tp -> LDiff a b -> Index b tp
ldiffIndex Index a tp
i LDiff a b
LDiffHere = Index a tp
Index b tp
i
ldiffIndex Index a tp
i (LDiffThere LDiff (a ::> x) b
d) = Index (a ::> x) tp -> LDiff (a ::> x) b -> Index b tp
forall {k} (a :: Ctx k) (tp :: k) (b :: Ctx k).
Index a tp -> LDiff a b -> Index b tp
ldiffIndex (Index a tp -> Index (a ::> x) tp
forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
IndexThere Index a tp
i) LDiff (a ::> x) b
d
forIndexLDiff :: Size a
-> LDiff a b
-> (forall tp . Index b tp -> r -> r)
-> r
-> r
forIndexLDiff :: forall {k} (a :: Ctx k) (b :: Ctx k) r.
Size a
-> LDiff a b -> (forall (tp :: k). Index b tp -> r -> r) -> r -> r
forIndexLDiff Size a
_ LDiff a b
LDiffHere forall (tp :: k). Index b tp -> r -> r
_ r
r = r
r
forIndexLDiff Size a
sz (LDiffThere LDiff (a ::> x) b
d) forall (tp :: k). Index b tp -> r -> r
f r
r =
Size (a ::> x)
-> LDiff (a ::> x) b
-> (forall (tp :: k). Index b tp -> r -> r)
-> r
-> r
forall {k} (a :: Ctx k) (b :: Ctx k) r.
Size a
-> LDiff a b -> (forall (tp :: k). Index b tp -> r -> r) -> r -> r
forIndexLDiff (Size a -> Size (a ::> x)
forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
SizeSucc Size a
sz) LDiff (a ::> x) b
d Index b tp -> r -> r
forall (tp :: k). Index b tp -> r -> r
f (Index b x -> r -> r
forall (tp :: k). Index b tp -> r -> r
f (Index (a ::> x) x -> LDiff (a ::> x) b -> Index b x
forall {k} (a :: Ctx k) (tp :: k) (b :: Ctx k).
Index a tp -> LDiff a b -> Index b tp
ldiffIndex (Size a -> Index (a ::> x) x
forall {k} (n :: Ctx k) (tp :: k). Size n -> Index (n '::> tp) tp
IndexHere Size a
sz) LDiff (a ::> x) b
d) r
r)
forIndexRangeImpl :: Int
-> Size a
-> LDiff a b
-> (forall tp . Index b tp -> r -> r)
-> r
-> r
forIndexRangeImpl :: forall {k} (a :: Ctx k) (b :: Ctx k) r.
Int
-> Size a
-> LDiff a b
-> (forall (tp :: k). Index b tp -> r -> r)
-> r
-> r
forIndexRangeImpl Int
0 Size a
sz LDiff a b
d forall (tp :: k). Index b tp -> r -> r
f r
r = Size a
-> LDiff a b -> (forall (tp :: k). Index b tp -> r -> r) -> r -> r
forall {k} (a :: Ctx k) (b :: Ctx k) r.
Size a
-> LDiff a b -> (forall (tp :: k). Index b tp -> r -> r) -> r -> r
forIndexLDiff Size a
sz LDiff a b
d Index b tp -> r -> r
forall (tp :: k). Index b tp -> r -> r
f r
r
forIndexRangeImpl Int
_ Size a
SizeZero LDiff a b
_ forall (tp :: k). Index b tp -> r -> r
_ r
r = r
r
forIndexRangeImpl Int
i (SizeSucc Size ctx
sz) LDiff a b
d forall (tp :: k). Index b tp -> r -> r
f r
r =
Int
-> Size ctx
-> LDiff ctx b
-> (forall (tp :: k). Index b tp -> r -> r)
-> r
-> r
forall {k} (a :: Ctx k) (b :: Ctx k) r.
Int
-> Size a
-> LDiff a b
-> (forall (tp :: k). Index b tp -> r -> r)
-> r
-> r
forIndexRangeImpl (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Size ctx
sz (LDiff (ctx '::> tp) b -> LDiff ctx b
forall {k} (a :: Ctx k) (n :: k) (b :: Ctx k).
LDiff (a ::> n) b -> LDiff a b
LDiffThere LDiff a b
LDiff (ctx '::> tp) b
d) Index b tp -> r -> r
forall (tp :: k). Index b tp -> r -> r
f r
r
forIndexRange :: Int
-> Size ctx
-> (forall tp . Index ctx tp -> r -> r)
-> r
-> r
forIndexRange :: forall {k} (ctx :: Ctx k) r.
Int
-> Size ctx -> (forall (tp :: k). Index ctx tp -> r -> r) -> r -> r
forIndexRange Int
i Size ctx
sz forall (tp :: k). Index ctx tp -> r -> r
f r
r = Int
-> Size ctx
-> LDiff ctx ctx
-> (forall (tp :: k). Index ctx tp -> r -> r)
-> r
-> r
forall {k} (a :: Ctx k) (b :: Ctx k) r.
Int
-> Size a
-> LDiff a b
-> (forall (tp :: k). Index b tp -> r -> r)
-> r
-> r
forIndexRangeImpl Int
i Size ctx
sz LDiff ctx ctx
forall {k} (a :: Ctx k). LDiff a a
LDiffHere Index ctx tp -> r -> r
forall (tp :: k). Index ctx tp -> r -> r
f r
r
indexList :: forall ctx. Size ctx -> [Some (Index ctx)]
indexList :: forall {k} (ctx :: Ctx k). Size ctx -> [Some (Index ctx)]
indexList Size ctx
sz_top = (forall (tp :: k). Index ctx tp -> Index ctx tp)
-> [Some (Index ctx)] -> Size ctx -> [Some (Index ctx)]
forall (ctx' :: Ctx k).
(forall (tp :: k). Index ctx' tp -> Index ctx tp)
-> [Some (Index ctx)] -> Size ctx' -> [Some (Index ctx)]
go Index ctx tp -> Index ctx tp
forall (tp :: k). Index ctx tp -> Index ctx tp
forall a. a -> a
id [] Size ctx
sz_top
where go :: (forall tp. Index ctx' tp -> Index ctx tp)
-> [Some (Index ctx)]
-> Size ctx'
-> [Some (Index ctx)]
go :: forall (ctx' :: Ctx k).
(forall (tp :: k). Index ctx' tp -> Index ctx tp)
-> [Some (Index ctx)] -> Size ctx' -> [Some (Index ctx)]
go forall (tp :: k). Index ctx' tp -> Index ctx tp
_ [Some (Index ctx)]
ls Size ctx'
SizeZero = [Some (Index ctx)]
ls
go forall (tp :: k). Index ctx' tp -> Index ctx tp
g [Some (Index ctx)]
ls (SizeSucc Size ctx
sz) = (forall (tp :: k). Index ctx tp -> Index ctx tp)
-> [Some (Index ctx)] -> Size ctx -> [Some (Index ctx)]
forall (ctx' :: Ctx k).
(forall (tp :: k). Index ctx' tp -> Index ctx tp)
-> [Some (Index ctx)] -> Size ctx' -> [Some (Index ctx)]
go (\Index ctx tp
i -> Index ctx' tp -> Index ctx tp
forall (tp :: k). Index ctx' tp -> Index ctx tp
g (Index ctx tp -> Index (ctx '::> tp) tp
forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
IndexThere Index ctx tp
i)) (Index ctx tp -> Some (Index ctx)
forall k (f :: k -> *) (x :: k). f x -> Some f
Some (Index ctx' tp -> Index ctx tp
forall (tp :: k). Index ctx' tp -> Index ctx tp
g (Size ctx -> Index (ctx '::> tp) tp
forall {k} (n :: Ctx k) (tp :: k). Size n -> Index (n '::> tp) tp
IndexHere Size ctx
sz)) Some (Index ctx) -> [Some (Index ctx)] -> [Some (Index ctx)]
forall a. a -> [a] -> [a]
: [Some (Index ctx)]
ls) Size ctx
sz
intIndex :: Int -> Size ctx -> Maybe (Some (Index ctx))
intIndex :: forall {k} (ctx :: Ctx k).
Int -> Size ctx -> Maybe (Some (Index ctx))
intIndex Int
n Size ctx
sz = [Some (Index ctx)] -> Maybe (Some (Index ctx))
forall a. [a] -> Maybe a
listToMaybe ([Some (Index ctx)] -> Maybe (Some (Index ctx)))
-> [Some (Index ctx)] -> Maybe (Some (Index ctx))
forall a b. (a -> b) -> a -> b
$ Int -> [Some (Index ctx)] -> [Some (Index ctx)]
forall a. Int -> [a] -> [a]
drop Int
n ([Some (Index ctx)] -> [Some (Index ctx)])
-> [Some (Index ctx)] -> [Some (Index ctx)]
forall a b. (a -> b) -> a -> b
$ Size ctx -> [Some (Index ctx)]
forall {k} (ctx :: Ctx k). Size ctx -> [Some (Index ctx)]
indexList Size ctx
sz
instance Show (Index ctx tp) where
show :: Index ctx tp -> String
show = Int -> String
forall a. Show a => a -> String
show (Int -> String) -> (Index ctx tp -> Int) -> Index ctx tp -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index ctx tp -> Int
forall {k} (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
indexVal
instance ShowF (Index ctx)
data IndexView ctx tp where
IndexViewLast :: Size ctx -> IndexView (ctx '::> t) t
IndexViewInit :: Index ctx t -> IndexView (ctx '::> u) t
instance ShowF (IndexView ctx)
deriving instance Show (IndexView ctx tp)
viewIndex :: Size ctx -> Index ctx tp -> IndexView ctx tp
viewIndex :: forall {k} (ctx :: Ctx k) (tp :: k).
Size ctx -> Index ctx tp -> IndexView ctx tp
viewIndex Size ctx
_ (IndexHere Size ctx
sz) = Size ctx -> IndexView (ctx '::> tp) tp
forall {k} (n :: Ctx k) (t :: k). Size n -> IndexView (n '::> t) t
IndexViewLast Size ctx
sz
viewIndex Size ctx
_ (IndexThere Index ctx tp
i) = Index ctx tp -> IndexView (ctx '::> tp') tp
forall {k} (n :: Ctx k) (t :: k) (tp :: k).
Index n t -> IndexView (n '::> tp) t
IndexViewInit Index ctx tp
i
data Assignment (f :: k -> Type) (ctx :: Ctx k) where
AssignmentEmpty :: Assignment f EmptyCtx
AssignmentExtend :: Assignment f ctx -> f tp -> Assignment f (ctx ::> tp)
data AssignView (f :: k -> Type) (ctx :: Ctx k) where
AssignEmpty :: AssignView f EmptyCtx
AssignExtend :: Assignment f ctx -> f tp -> AssignView f (ctx::>tp)
viewAssign :: forall f ctx . Assignment f ctx -> AssignView f ctx
viewAssign :: forall {k} (f :: k -> *) (ctx :: Ctx k).
Assignment f ctx -> AssignView f ctx
viewAssign Assignment f ctx
AssignmentEmpty = AssignView f ctx
AssignView f 'EmptyCtx
forall {k} (f :: k -> *). AssignView f EmptyCtx
AssignEmpty
viewAssign (AssignmentExtend Assignment f ctx
asgn f tp
x) = Assignment f ctx -> f tp -> AssignView f (ctx '::> tp)
forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
Assignment f n -> f tp -> AssignView f (n ::> tp)
AssignExtend Assignment f ctx
asgn f tp
x
instance NFData (Assignment f ctx) where
rnf :: Assignment f ctx -> ()
rnf Assignment f ctx
AssignmentEmpty = ()
rnf (AssignmentExtend Assignment f ctx
asgn f tp
x) = Assignment f ctx -> ()
forall a. NFData a => a -> ()
rnf Assignment f ctx
asgn () -> () -> ()
forall a b. a -> b -> b
`seq` f tp
x f tp -> () -> ()
forall a b. a -> b -> b
`seq` ()
size :: Assignment f ctx -> Size ctx
size :: forall {k} (f :: k -> *) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
size Assignment f ctx
AssignmentEmpty = Size ctx
Size 'EmptyCtx
forall {k}. Size 'EmptyCtx
SizeZero
size (AssignmentExtend Assignment f ctx
asgn f tp
_) = Size ctx -> Size (ctx '::> tp)
forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
SizeSucc (Assignment f ctx -> Size ctx
forall {k} (f :: k -> *) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
size Assignment f ctx
asgn)
generate :: forall ctx f
. Size ctx
-> (forall tp . Index ctx tp -> f tp)
-> Assignment f ctx
generate :: forall {k} (ctx :: Ctx k) (f :: k -> *).
Size ctx
-> (forall (tp :: k). Index ctx tp -> f tp) -> Assignment f ctx
generate Size ctx
sz_top forall (tp :: k). Index ctx tp -> f tp
f = (forall (tp :: k). Index ctx tp -> Index ctx tp)
-> Size ctx -> Assignment f ctx
forall (ctx' :: Ctx k).
(forall (tp :: k). Index ctx' tp -> Index ctx tp)
-> Size ctx' -> Assignment f ctx'
go Index ctx tp -> Index ctx tp
forall (tp :: k). Index ctx tp -> Index ctx tp
forall a. a -> a
id Size ctx
sz_top
where go :: forall ctx'
. (forall tp. Index ctx' tp -> Index ctx tp)
-> Size ctx'
-> Assignment f ctx'
go :: forall (ctx' :: Ctx k).
(forall (tp :: k). Index ctx' tp -> Index ctx tp)
-> Size ctx' -> Assignment f ctx'
go forall (tp :: k). Index ctx' tp -> Index ctx tp
_ Size ctx'
SizeZero = Assignment f ctx'
Assignment f 'EmptyCtx
forall {k} (f :: k -> *). Assignment f EmptyCtx
AssignmentEmpty
go forall (tp :: k). Index ctx' tp -> Index ctx tp
g (SizeSucc Size ctx
sz) =
let ctx :: Assignment f ctx
ctx = (forall (tp :: k). Index ctx tp -> Index ctx tp)
-> Size ctx -> Assignment f ctx
forall (ctx' :: Ctx k).
(forall (tp :: k). Index ctx' tp -> Index ctx tp)
-> Size ctx' -> Assignment f ctx'
go (\Index ctx tp
i -> Index ctx' tp -> Index ctx tp
forall (tp :: k). Index ctx' tp -> Index ctx tp
g (Index ctx tp -> Index (ctx '::> tp) tp
forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
IndexThere Index ctx tp
i)) Size ctx
sz
x :: f tp
x = Index ctx tp -> f tp
forall (tp :: k). Index ctx tp -> f tp
f (Index ctx' tp -> Index ctx tp
forall (tp :: k). Index ctx' tp -> Index ctx tp
g (Size ctx -> Index (ctx '::> tp) tp
forall {k} (n :: Ctx k) (tp :: k). Size n -> Index (n '::> tp) tp
IndexHere Size ctx
sz))
in Assignment f ctx -> f tp -> Assignment f (ctx '::> tp)
forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
Assignment f n -> f tp -> Assignment f (n ::> tp)
AssignmentExtend Assignment f ctx
ctx f tp
x
generateM :: forall ctx m f
. Applicative m
=> Size ctx
-> (forall tp . Index ctx tp -> m (f tp))
-> m (Assignment f ctx)
generateM :: forall {k} (ctx :: Ctx k) (m :: * -> *) (f :: k -> *).
Applicative m =>
Size ctx
-> (forall (tp :: k). Index ctx tp -> m (f tp))
-> m (Assignment f ctx)
generateM Size ctx
sz_top forall (tp :: k). Index ctx tp -> m (f tp)
f = (forall (tp :: k). Index ctx tp -> Index ctx tp)
-> Size ctx -> m (Assignment f ctx)
forall (ctx' :: Ctx k).
(forall (tp :: k). Index ctx' tp -> Index ctx tp)
-> Size ctx' -> m (Assignment f ctx')
go Index ctx tp -> Index ctx tp
forall (tp :: k). Index ctx tp -> Index ctx tp
forall a. a -> a
id Size ctx
sz_top
where go :: forall ctx'. (forall tp. Index ctx' tp -> Index ctx tp) -> Size ctx' -> m (Assignment f ctx')
go :: forall (ctx' :: Ctx k).
(forall (tp :: k). Index ctx' tp -> Index ctx tp)
-> Size ctx' -> m (Assignment f ctx')
go forall (tp :: k). Index ctx' tp -> Index ctx tp
_ Size ctx'
SizeZero = Assignment f ctx' -> m (Assignment f ctx')
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Assignment f ctx'
Assignment f 'EmptyCtx
forall {k} (f :: k -> *). Assignment f EmptyCtx
AssignmentEmpty
go forall (tp :: k). Index ctx' tp -> Index ctx tp
g (SizeSucc Size ctx
sz) =
Assignment f ctx -> f tp -> Assignment f ctx'
Assignment f ctx -> f tp -> Assignment f (ctx '::> tp)
forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
Assignment f n -> f tp -> Assignment f (n ::> tp)
AssignmentExtend (Assignment f ctx -> f tp -> Assignment f ctx')
-> m (Assignment f ctx) -> m (f tp -> Assignment f ctx')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((forall (tp :: k). Index ctx tp -> Index ctx tp)
-> Size ctx -> m (Assignment f ctx)
forall (ctx' :: Ctx k).
(forall (tp :: k). Index ctx' tp -> Index ctx tp)
-> Size ctx' -> m (Assignment f ctx')
go (\Index ctx tp
i -> Index ctx' tp -> Index ctx tp
forall (tp :: k). Index ctx' tp -> Index ctx tp
g (Index ctx tp -> Index (ctx '::> tp) tp
forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
IndexThere Index ctx tp
i)) Size ctx
sz) m (f tp -> Assignment f ctx') -> m (f tp) -> m (Assignment f ctx')
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Index ctx tp -> m (f tp)
forall (tp :: k). Index ctx tp -> m (f tp)
f (Index ctx' tp -> Index ctx tp
forall (tp :: k). Index ctx' tp -> Index ctx tp
g (Size ctx -> Index (ctx '::> tp) tp
forall {k} (n :: Ctx k) (tp :: k). Size n -> Index (n '::> tp) tp
IndexHere Size ctx
sz))
replicate :: Size ctx -> (forall tp . f tp) -> Assignment f ctx
replicate :: forall {k} (ctx :: Ctx k) (f :: k -> *).
Size ctx -> (forall (tp :: k). f tp) -> Assignment f ctx
replicate Size ctx
n forall (tp :: k). f tp
c = Size ctx
-> (forall (tp :: k). Index ctx tp -> f tp) -> Assignment f ctx
forall {k} (ctx :: Ctx k) (f :: k -> *).
Size ctx
-> (forall (tp :: k). Index ctx tp -> f tp) -> Assignment f ctx
generate Size ctx
n (\Index ctx tp
_ -> f tp
forall (tp :: k). f tp
c)
empty :: Assignment f 'EmptyCtx
empty :: forall {k} (f :: k -> *). Assignment f EmptyCtx
empty = Assignment f EmptyCtx
forall {k} (f :: k -> *). Assignment f EmptyCtx
AssignmentEmpty
extend :: Assignment f ctx -> f tp -> Assignment f (ctx '::> tp)
extend :: forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
Assignment f n -> f tp -> Assignment f (n ::> tp)
extend Assignment f ctx
asgn f tp
e = Assignment f ctx -> f tp -> Assignment f (ctx ::> tp)
forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
Assignment f n -> f tp -> Assignment f (n ::> tp)
AssignmentExtend Assignment f ctx
asgn f tp
e
{-# DEPRECATED adjust "Replace 'adjust f i asgn' with 'Lens.over (ixF i) f asgn' instead." #-}
adjust :: forall f ctx tp. (f tp -> f tp) -> Index ctx tp -> Assignment f ctx -> Assignment f ctx
adjust :: forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(f tp -> f tp)
-> Index ctx tp -> Assignment f ctx -> Assignment f ctx
adjust f tp -> f tp
f Index ctx tp
idx Assignment f ctx
asgn = Identity (Assignment f ctx) -> Assignment f ctx
forall a. Identity a -> a
runIdentity ((f tp -> Identity (f tp))
-> Index ctx tp -> Assignment f ctx -> Identity (Assignment f ctx)
forall {k} (m :: * -> *) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Functor m =>
(f tp -> m (f tp))
-> Index ctx tp -> Assignment f ctx -> m (Assignment f ctx)
adjustM (f tp -> Identity (f tp)
forall a. a -> Identity a
Identity (f tp -> Identity (f tp))
-> (f tp -> f tp) -> f tp -> Identity (f tp)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f tp -> f tp
f) Index ctx tp
idx Assignment f ctx
asgn)
{-# DEPRECATED update "Replace 'update idx val asgn' with 'Lens.set (ixF idx) val asgn' instead." #-}
update :: forall f ctx tp. Index ctx tp -> f tp -> Assignment f ctx -> Assignment f ctx
update :: forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Index ctx tp -> f tp -> Assignment f ctx -> Assignment f ctx
update Index ctx tp
i f tp
v Assignment f ctx
a = (f tp -> f tp)
-> Index ctx tp -> Assignment f ctx -> Assignment f ctx
forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(f tp -> f tp)
-> Index ctx tp -> Assignment f ctx -> Assignment f ctx
adjust (\f tp
_ -> f tp
v) Index ctx tp
i Assignment f ctx
a
adjustM :: forall m f ctx tp. Functor m => (f tp -> m (f tp)) -> Index ctx tp -> Assignment f ctx -> m (Assignment f ctx)
adjustM :: forall {k} (m :: * -> *) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Functor m =>
(f tp -> m (f tp))
-> Index ctx tp -> Assignment f ctx -> m (Assignment f ctx)
adjustM f tp -> m (f tp)
f = (forall (tp' :: k). f tp' -> f tp')
-> Index ctx tp -> Assignment f ctx -> m (Assignment f ctx)
forall (g :: k -> *) (ctx' :: Ctx k).
(forall (tp' :: k). g tp' -> f tp')
-> Index ctx' tp -> Assignment g ctx' -> m (Assignment f ctx')
go (\f tp'
x -> f tp'
x)
where
go :: (forall tp'. g tp' -> f tp') -> Index ctx' tp -> Assignment g ctx' -> m (Assignment f ctx')
go :: forall (g :: k -> *) (ctx' :: Ctx k).
(forall (tp' :: k). g tp' -> f tp')
-> Index ctx' tp -> Assignment g ctx' -> m (Assignment f ctx')
go forall (tp' :: k). g tp' -> f tp'
g (IndexHere Size ctx
_) (AssignmentExtend Assignment g ctx
asgn g tp
x) = Assignment f ctx -> f tp -> Assignment f (ctx ::> tp)
forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
Assignment f n -> f tp -> Assignment f (n ::> tp)
AssignmentExtend ((forall (tp' :: k). g tp' -> f tp')
-> Assignment g ctx -> Assignment f ctx
forall {k} (f :: k -> *) (g :: k -> *) (c :: Ctx k).
(forall (tp :: k). f tp -> g tp)
-> Assignment f c -> Assignment g c
map g tp -> f tp
forall (tp' :: k). g tp' -> f tp'
g Assignment g ctx
asgn) (f tp -> Assignment f ctx') -> m (f tp) -> m (Assignment f ctx')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f tp -> m (f tp)
f (g tp -> f tp
forall (tp' :: k). g tp' -> f tp'
g g tp
g tp
x)
go forall (tp' :: k). g tp' -> f tp'
g (IndexThere Index ctx tp
idx) (AssignmentExtend Assignment g ctx
asgn g tp
x) = (Assignment f ctx -> f tp -> Assignment f ctx')
-> f tp -> Assignment f ctx -> Assignment f ctx'
forall a b c. (a -> b -> c) -> b -> a -> c
flip Assignment f ctx -> f tp -> Assignment f ctx'
Assignment f ctx -> f tp -> Assignment f (ctx ::> tp)
forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
Assignment f n -> f tp -> Assignment f (n ::> tp)
AssignmentExtend (g tp -> f tp
forall (tp' :: k). g tp' -> f tp'
g g tp
x) (Assignment f ctx -> Assignment f ctx')
-> m (Assignment f ctx) -> m (Assignment f ctx')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (tp' :: k). g tp' -> f tp')
-> Index ctx tp -> Assignment g ctx -> m (Assignment f ctx)
forall (g :: k -> *) (ctx' :: Ctx k).
(forall (tp' :: k). g tp' -> f tp')
-> Index ctx' tp -> Assignment g ctx' -> m (Assignment f ctx')
go g tp' -> f tp'
forall (tp' :: k). g tp' -> f tp'
g Index ctx tp
idx Assignment g ctx
Assignment g ctx
asgn
type instance IndexF (Assignment (f :: k -> Type) ctx) = Index ctx
type instance IxValueF (Assignment (f :: k -> Type) ctx) = f
instance forall k (f :: k -> Type) ctx. IxedF k (Assignment f ctx) where
ixF :: Index ctx x -> Lens.Traversal' (Assignment f ctx) (f x)
ixF :: forall (x :: k). Index ctx x -> Traversal' (Assignment f ctx) (f x)
ixF Index ctx x
idx f x -> f (f x)
f = (f x -> f (f x))
-> Index ctx x -> Assignment f ctx -> f (Assignment f ctx)
forall {k} (m :: * -> *) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Functor m =>
(f tp -> m (f tp))
-> Index ctx tp -> Assignment f ctx -> m (Assignment f ctx)
adjustM f x -> f (f x)
f Index ctx x
idx
instance forall k (f :: k -> Type) ctx. IxedF' k (Assignment f ctx) where
ixF' :: Index ctx x -> Lens.Lens' (Assignment f ctx) (f x)
ixF' :: forall (x :: k). Index ctx x -> Lens' (Assignment f ctx) (f x)
ixF' Index ctx x
idx f x -> f (f x)
f = (f x -> f (f x))
-> Index ctx x -> Assignment f ctx -> f (Assignment f ctx)
forall {k} (m :: * -> *) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Functor m =>
(f tp -> m (f tp))
-> Index ctx tp -> Assignment f ctx -> m (Assignment f ctx)
adjustM f x -> f (f x)
f Index ctx x
idx
idxlookup :: (forall tp. a tp -> b tp) -> Assignment a ctx -> forall tp. Index ctx tp -> b tp
idxlookup :: forall {k} (a :: k -> *) (b :: k -> *) (ctx :: Ctx k).
(forall (tp :: k). a tp -> b tp)
-> Assignment a ctx -> forall (tp :: k). Index ctx tp -> b tp
idxlookup forall (tp :: k). a tp -> b tp
f (AssignmentExtend Assignment a ctx
_ a tp
x) (IndexHere Size ctx
_) = a tp -> b tp
forall (tp :: k). a tp -> b tp
f a tp
a tp
x
idxlookup forall (tp :: k). a tp -> b tp
f (AssignmentExtend Assignment a ctx
ctx a tp
_) (IndexThere Index ctx tp
idx) = (forall (tp :: k). a tp -> b tp)
-> Assignment a ctx -> forall (tp :: k). Index ctx tp -> b tp
forall {k} (a :: k -> *) (b :: k -> *) (ctx :: Ctx k).
(forall (tp :: k). a tp -> b tp)
-> Assignment a ctx -> forall (tp :: k). Index ctx tp -> b tp
idxlookup a tp -> b tp
forall (tp :: k). a tp -> b tp
f Assignment a ctx
ctx Index ctx tp
Index ctx tp
idx
idxlookup forall (tp :: k). a tp -> b tp
_ Assignment a ctx
AssignmentEmpty Index ctx tp
idx = case Index ctx tp
idx of {}
(!) :: Assignment f ctx -> Index ctx tp -> f tp
! :: forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
(!) Assignment f ctx
asgn Index ctx tp
idx = (forall (tp :: k). f tp -> f tp)
-> Assignment f ctx -> forall (tp :: k). Index ctx tp -> f tp
forall {k} (a :: k -> *) (b :: k -> *) (ctx :: Ctx k).
(forall (tp :: k). a tp -> b tp)
-> Assignment a ctx -> forall (tp :: k). Index ctx tp -> b tp
idxlookup f tp -> f tp
forall (tp :: k). f tp -> f tp
forall a. a -> a
id Assignment f ctx
asgn Index ctx tp
idx
(!^) :: KnownDiff l r => Assignment f r -> Index l tp -> f tp
Assignment f r
a !^ :: forall {k} (l :: Ctx k) (r :: Ctx k) (f :: k -> *) (tp :: k).
KnownDiff l r =>
Assignment f r -> Index l tp -> f tp
!^ Index l tp
i = Assignment f r
a Assignment f r -> Index r tp -> f tp
forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
! Index l tp -> Index r tp
forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
KnownDiff l r =>
Index l tp -> Index r tp
extendIndex Index l tp
i
instance TestEquality f => Eq (Assignment f ctx) where
Assignment f ctx
x == :: Assignment f ctx -> Assignment f ctx -> Bool
== Assignment f ctx
y = Maybe (ctx :~: ctx) -> Bool
forall a. Maybe a -> Bool
isJust (Assignment f ctx -> Assignment f ctx -> Maybe (ctx :~: ctx)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Ctx k) (b :: Ctx k).
Assignment f a -> Assignment f b -> Maybe (a :~: b)
testEquality Assignment f ctx
x Assignment f ctx
y)
testEq :: (forall x y. f x -> f y -> Maybe (x :~: y))
-> Assignment f cxt1 -> Assignment f cxt2 -> Maybe (cxt1 :~: cxt2)
testEq :: forall {k} (f :: k -> *) (cxt1 :: Ctx k) (cxt2 :: Ctx k).
(forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
-> Assignment f cxt1 -> Assignment f cxt2 -> Maybe (cxt1 :~: cxt2)
testEq forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
_ Assignment f cxt1
AssignmentEmpty Assignment f cxt2
AssignmentEmpty = (cxt1 :~: cxt2) -> Maybe (cxt1 :~: cxt2)
forall a. a -> Maybe a
Just cxt1 :~: cxt1
cxt1 :~: cxt2
forall {k} (a :: k). a :~: a
Refl
testEq forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
test (AssignmentExtend Assignment f ctx
ctx1 f tp
x1) (AssignmentExtend Assignment f ctx
ctx2 f tp
x2) =
case (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
-> Assignment f ctx -> Assignment f ctx -> Maybe (ctx :~: ctx)
forall {k} (f :: k -> *) (cxt1 :: Ctx k) (cxt2 :: Ctx k).
(forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
-> Assignment f cxt1 -> Assignment f cxt2 -> Maybe (cxt1 :~: cxt2)
testEq f x -> f y -> Maybe (x :~: y)
forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
test Assignment f ctx
ctx1 Assignment f ctx
ctx2 of
Maybe (ctx :~: ctx)
Nothing -> Maybe (cxt1 :~: cxt2)
forall a. Maybe a
Nothing
Just ctx :~: ctx
Refl ->
case f tp -> f tp -> Maybe (tp :~: tp)
forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
test f tp
x1 f tp
x2 of
Maybe (tp :~: tp)
Nothing -> Maybe (cxt1 :~: cxt2)
forall a. Maybe a
Nothing
Just tp :~: tp
Refl -> (cxt1 :~: cxt2) -> Maybe (cxt1 :~: cxt2)
forall a. a -> Maybe a
Just cxt1 :~: cxt1
cxt1 :~: cxt2
forall {k} (a :: k). a :~: a
Refl
testEq forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
_ Assignment f cxt1
AssignmentEmpty AssignmentExtend{} = Maybe (cxt1 :~: cxt2)
forall a. Maybe a
Nothing
testEq forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
_ AssignmentExtend{} Assignment f cxt2
AssignmentEmpty = Maybe (cxt1 :~: cxt2)
forall a. Maybe a
Nothing
instance TestEqualityFC Assignment where
testEqualityFC :: forall (f :: k -> *).
(forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
-> forall (x :: Ctx k) (y :: Ctx k).
Assignment f x -> Assignment f y -> Maybe (x :~: y)
testEqualityFC forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
f = (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
-> Assignment f x -> Assignment f y -> Maybe (x :~: y)
forall {k} (f :: k -> *) (cxt1 :: Ctx k) (cxt2 :: Ctx k).
(forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
-> Assignment f cxt1 -> Assignment f cxt2 -> Maybe (cxt1 :~: cxt2)
testEq f x -> f y -> Maybe (x :~: y)
forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
f
instance TestEquality f => TestEquality (Assignment f) where
testEquality :: forall (a :: Ctx k) (b :: Ctx k).
Assignment f a -> Assignment f b -> Maybe (a :~: b)
testEquality Assignment f a
x Assignment f b
y = (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
-> Assignment f a -> Assignment f b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (cxt1 :: Ctx k) (cxt2 :: Ctx k).
(forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
-> Assignment f cxt1 -> Assignment f cxt2 -> Maybe (cxt1 :~: cxt2)
testEq f x -> f y -> Maybe (x :~: y)
forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Assignment f a
x Assignment f b
y
instance TestEquality f => PolyEq (Assignment f x) (Assignment f y) where
polyEqF :: Assignment f x
-> Assignment f y -> Maybe (Assignment f x :~: Assignment f y)
polyEqF Assignment f x
x Assignment f y
y = ((x :~: y) -> Assignment f x :~: Assignment f y)
-> Maybe (x :~: y) -> Maybe (Assignment f x :~: Assignment f y)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\x :~: y
Refl -> Assignment f x :~: Assignment f x
Assignment f x :~: Assignment f y
forall {k} (a :: k). a :~: a
Refl) (Maybe (x :~: y) -> Maybe (Assignment f x :~: Assignment f y))
-> Maybe (x :~: y) -> Maybe (Assignment f x :~: Assignment f y)
forall a b. (a -> b) -> a -> b
$ Assignment f x -> Assignment f y -> Maybe (x :~: y)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Ctx k) (b :: Ctx k).
Assignment f a -> Assignment f b -> Maybe (a :~: b)
testEquality Assignment f x
x Assignment f y
y
compareAsgn :: (forall x y. f x -> f y -> OrderingF x y)
-> Assignment f ctx1 -> Assignment f ctx2 -> OrderingF ctx1 ctx2
compareAsgn :: forall {k} (f :: k -> *) (ctx1 :: Ctx k) (ctx2 :: Ctx k).
(forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
-> Assignment f ctx1 -> Assignment f ctx2 -> OrderingF ctx1 ctx2
compareAsgn forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
_ Assignment f ctx1
AssignmentEmpty Assignment f ctx2
AssignmentEmpty = OrderingF ctx1 ctx1
OrderingF ctx1 ctx2
forall {k} (x :: k). OrderingF x x
EQF
compareAsgn forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
_ Assignment f ctx1
AssignmentEmpty Assignment f ctx2
_ = OrderingF ctx1 ctx2
forall {k} (x :: k) (y :: k). OrderingF x y
GTF
compareAsgn forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
_ Assignment f ctx1
_ Assignment f ctx2
AssignmentEmpty = OrderingF ctx1 ctx2
forall {k} (x :: k) (y :: k). OrderingF x y
LTF
compareAsgn forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
test (AssignmentExtend Assignment f ctx
ctx1 f tp
x) (AssignmentExtend Assignment f ctx
ctx2 f tp
y) =
case (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
-> Assignment f ctx -> Assignment f ctx -> OrderingF ctx ctx
forall {k} (f :: k -> *) (ctx1 :: Ctx k) (ctx2 :: Ctx k).
(forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
-> Assignment f ctx1 -> Assignment f ctx2 -> OrderingF ctx1 ctx2
compareAsgn f x -> f y -> OrderingF x y
forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
test Assignment f ctx
ctx1 Assignment f ctx
ctx2 of
OrderingF ctx ctx
LTF -> OrderingF ctx1 ctx2
forall {k} (x :: k) (y :: k). OrderingF x y
LTF
OrderingF ctx ctx
GTF -> OrderingF ctx1 ctx2
forall {k} (x :: k) (y :: k). OrderingF x y
GTF
OrderingF ctx ctx
EQF -> case f tp -> f tp -> OrderingF tp tp
forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
test f tp
x f tp
y of
OrderingF tp tp
LTF -> OrderingF ctx1 ctx2
forall {k} (x :: k) (y :: k). OrderingF x y
LTF
OrderingF tp tp
GTF -> OrderingF ctx1 ctx2
forall {k} (x :: k) (y :: k). OrderingF x y
GTF
OrderingF tp tp
EQF -> OrderingF ctx1 ctx1
OrderingF ctx1 ctx2
forall {k} (x :: k). OrderingF x x
EQF
instance OrdFC Assignment where
compareFC :: forall (f :: k -> *).
(forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
-> forall (x :: Ctx k) (y :: Ctx k).
Assignment f x -> Assignment f y -> OrderingF x y
compareFC forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
f = (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
-> Assignment f x -> Assignment f y -> OrderingF x y
forall {k} (f :: k -> *) (ctx1 :: Ctx k) (ctx2 :: Ctx k).
(forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
-> Assignment f ctx1 -> Assignment f ctx2 -> OrderingF ctx1 ctx2
compareAsgn f x -> f y -> OrderingF x y
forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
f
instance OrdF f => OrdF (Assignment f) where
compareF :: forall (x :: Ctx k) (y :: Ctx k).
Assignment f x -> Assignment f y -> OrderingF x y
compareF = (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
-> Assignment f x -> Assignment f y -> OrderingF x y
forall {k} (f :: k -> *) (ctx1 :: Ctx k) (ctx2 :: Ctx k).
(forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
-> Assignment f ctx1 -> Assignment f ctx2 -> OrderingF ctx1 ctx2
compareAsgn f x -> f y -> OrderingF x y
forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
forall k (ktp :: k -> *) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF
instance OrdF f => Ord (Assignment f ctx) where
compare :: Assignment f ctx -> Assignment f ctx -> Ordering
compare Assignment f ctx
x Assignment f ctx
y = OrderingF ctx ctx -> Ordering
forall {k} (x :: k) (y :: k). OrderingF x y -> Ordering
toOrdering (Assignment f ctx -> Assignment f ctx -> OrderingF ctx ctx
forall k (ktp :: k -> *) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: Ctx k) (y :: Ctx k).
Assignment f x -> Assignment f y -> OrderingF x y
compareF Assignment f ctx
x Assignment f ctx
y)
instance Hashable (Index ctx tp) where
hashWithSalt :: Int -> Index ctx tp -> Int
hashWithSalt = Int -> Index ctx tp -> Int
forall (tp :: k). Int -> Index ctx tp -> Int
forall k (f :: k -> *) (tp :: k). HashableF f => Int -> f tp -> Int
hashWithSaltF
instance HashableF (Index ctx) where
hashWithSaltF :: forall (tp :: k). Int -> Index ctx tp -> Int
hashWithSaltF Int
s Index ctx tp
i = Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s (Index ctx tp -> Int
forall {k} (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
indexVal Index ctx tp
i)
instance (HashableF f, TestEquality f) => HashableF (Assignment f) where
hashWithSaltF :: forall (tp :: Ctx k). Int -> Assignment f tp -> Int
hashWithSaltF = Int -> Assignment f tp -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt
instance (HashableF f, TestEquality f) => Hashable (Assignment f ctx) where
hashWithSalt :: Int -> Assignment f ctx -> Int
hashWithSalt Int
s Assignment f ctx
AssignmentEmpty = Int
s
hashWithSalt Int
s (AssignmentExtend Assignment f ctx
asgn f tp
x) = (Int
s Int -> Assignment f ctx -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Assignment f ctx
asgn) Int -> f tp -> Int
forall (tp :: k). Int -> f tp -> Int
forall k (f :: k -> *) (tp :: k). HashableF f => Int -> f tp -> Int
`hashWithSaltF` f tp
x
instance ShowF f => Show (Assignment f ctx) where
show :: Assignment f ctx -> String
show Assignment f ctx
a = String
"[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ((forall (tp :: k). f tp -> String) -> Assignment f ctx -> [String]
forall {k} (f :: k -> *) a (c :: Ctx k).
(forall (tp :: k). f tp -> a) -> Assignment f c -> [a]
toList f tp -> String
forall (tp :: k). f tp -> String
forall k (f :: k -> *) (tp :: k). ShowF f => f tp -> String
showF Assignment f ctx
a) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"
instance ShowF f => ShowF (Assignment f)
instance FunctorFC Assignment where
fmapFC :: forall (f :: k -> *) (g :: k -> *).
(forall (x :: k). f x -> g x)
-> forall (x :: Ctx k). Assignment f x -> Assignment g x
fmapFC = (forall (x :: k). f x -> g x) -> Assignment f x -> Assignment g x
(forall (x :: k). f x -> g x)
-> forall (x :: Ctx k). Assignment f x -> Assignment g x
forall {k} {l} (t :: (k -> *) -> l -> *) (f :: k -> *)
(g :: k -> *).
TraversableFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: k -> *) (g :: k -> *).
(forall (x :: k). f x -> g x)
-> forall (x :: Ctx k). Assignment f x -> Assignment g x
fmapFCDefault
instance FoldableFC Assignment where
foldMapFC :: forall (f :: k -> *) m.
Monoid m =>
(forall (x :: k). f x -> m)
-> forall (x :: Ctx k). Assignment f x -> m
foldMapFC = (forall (x :: k). f x -> m) -> Assignment f x -> m
(forall (x :: k). f x -> m)
-> forall (x :: Ctx k). Assignment f x -> m
forall {k} {l} (t :: (k -> *) -> l -> *) m (f :: k -> *).
(TraversableFC t, Monoid m) =>
(forall (x :: k). f x -> m) -> forall (x :: l). t f x -> m
foldMapFCDefault
instance TraversableFC Assignment where
traverseFC :: forall (f :: k -> *) (g :: k -> *) (m :: * -> *).
Applicative m =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: Ctx k). Assignment f x -> m (Assignment g x)
traverseFC forall (x :: k). f x -> m (g x)
f = (forall (x :: k). f x -> m (g x))
-> Assignment f x -> m (Assignment g x)
forall k (f :: k -> *) (g :: k -> *) (m :: * -> *) (c :: Ctx k).
Applicative m =>
(forall (tp :: k). f tp -> m (g tp))
-> Assignment f c -> m (Assignment g c)
traverseF f tp -> m (g tp)
forall (x :: k). f x -> m (g x)
f
instance FunctorFCWithIndex Assignment where
imapFC :: forall (f :: k -> *) (g :: k -> *) (z :: Ctx k).
(forall (x :: k). IndexF (Assignment f z) x -> f x -> g x)
-> Assignment f z -> Assignment g z
imapFC = (forall (x :: k). IndexF (Assignment f z) x -> f x -> g x)
-> Assignment f z -> Assignment g z
forall {k} {l} (t :: (k -> *) -> l -> *) (f :: k -> *)
(g :: k -> *) (z :: l).
TraversableFCWithIndex t =>
(forall (x :: k). IndexF (t f z) x -> f x -> g x) -> t f z -> t g z
imapFCDefault
instance FoldableFCWithIndex Assignment where
ifoldMapFC :: forall (f :: k -> *) m (z :: Ctx k).
Monoid m =>
(forall (x :: k). IndexF (Assignment f z) x -> f x -> m)
-> Assignment f z -> m
ifoldMapFC = (forall (x :: k). IndexF (Assignment f z) x -> f x -> m)
-> Assignment f z -> m
forall {k} {l} (t :: (k -> *) -> l -> *) m (z :: l) (f :: k -> *).
(TraversableFCWithIndex t, Monoid m) =>
(forall (x :: k). IndexF (t f z) x -> f x -> m) -> t f z -> m
ifoldMapFCDefault
instance TraversableFCWithIndex Assignment where
itraverseFC :: forall (m :: * -> *) (z :: Ctx k) (f :: k -> *) (g :: k -> *).
Applicative m =>
(forall (x :: k). IndexF (Assignment f z) x -> f x -> m (g x))
-> Assignment f z -> m (Assignment g z)
itraverseFC = (forall (x :: k). IndexF (Assignment f z) x -> f x -> m (g x))
-> Assignment f z -> m (Assignment g z)
(forall (tp :: k). Index z tp -> f tp -> m (g tp))
-> Assignment f z -> m (Assignment g z)
forall {k} (m :: * -> *) (ctx :: Ctx k) (f :: k -> *)
(g :: k -> *).
Applicative m =>
(forall (tp :: k). Index ctx tp -> f tp -> m (g tp))
-> Assignment f ctx -> m (Assignment g ctx)
traverseWithIndex
map :: (forall tp . f tp -> g tp) -> Assignment f c -> Assignment g c
map :: forall {k} (f :: k -> *) (g :: k -> *) (c :: Ctx k).
(forall (tp :: k). f tp -> g tp)
-> Assignment f c -> Assignment g c
map forall (tp :: k). f tp -> g tp
f = (forall (tp :: k). f tp -> g tp)
-> forall (x :: Ctx k). Assignment f x -> Assignment g x
forall k l (t :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: k -> *) (g :: k -> *).
(forall (x :: k). f x -> g x)
-> forall (x :: Ctx k). Assignment f x -> Assignment g x
fmapFC f x -> g x
forall (tp :: k). f tp -> g tp
f
traverseF :: forall k (f:: k -> Type) (g::k -> Type) (m:: Type -> Type) (c::Ctx k)
. Applicative m
=> (forall tp . f tp -> m (g tp))
-> Assignment f c
-> m (Assignment g c)
traverseF :: forall k (f :: k -> *) (g :: k -> *) (m :: * -> *) (c :: Ctx k).
Applicative m =>
(forall (tp :: k). f tp -> m (g tp))
-> Assignment f c -> m (Assignment g c)
traverseF forall (tp :: k). f tp -> m (g tp)
_ Assignment f c
AssignmentEmpty = Assignment g c -> m (Assignment g c)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Assignment g c
Assignment g 'EmptyCtx
forall {k} (f :: k -> *). Assignment f EmptyCtx
AssignmentEmpty
traverseF forall (tp :: k). f tp -> m (g tp)
f (AssignmentExtend Assignment f ctx
asgn f tp
x) = (Assignment g ctx -> g tp -> Assignment g c)
-> m (Assignment g ctx -> g tp -> Assignment g c)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Assignment g ctx -> g tp -> Assignment g c
Assignment g ctx -> g tp -> Assignment g (ctx '::> tp)
forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
Assignment f n -> f tp -> Assignment f (n ::> tp)
AssignmentExtend m (Assignment g ctx -> g tp -> Assignment g c)
-> m (Assignment g ctx) -> m (g tp -> Assignment g c)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall (tp :: k). f tp -> m (g tp))
-> Assignment f ctx -> m (Assignment g ctx)
forall k (f :: k -> *) (g :: k -> *) (m :: * -> *) (c :: Ctx k).
Applicative m =>
(forall (tp :: k). f tp -> m (g tp))
-> Assignment f c -> m (Assignment g c)
traverseF f tp -> m (g tp)
forall (tp :: k). f tp -> m (g tp)
f Assignment f ctx
asgn m (g tp -> Assignment g c) -> m (g tp) -> m (Assignment g c)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f tp -> m (g tp)
forall (tp :: k). f tp -> m (g tp)
f f tp
x
toList :: (forall tp . f tp -> a)
-> Assignment f c
-> [a]
toList :: forall {k} (f :: k -> *) a (c :: Ctx k).
(forall (tp :: k). f tp -> a) -> Assignment f c -> [a]
toList forall (tp :: k). f tp -> a
f = (forall (tp :: k). f tp -> a)
-> forall (x :: Ctx k). Assignment f x -> [a]
forall k l (t :: (k -> *) -> l -> *) (f :: k -> *) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
forall (f :: k -> *) a.
(forall (x :: k). f x -> a)
-> forall (x :: Ctx k). Assignment f x -> [a]
toListFC f x -> a
forall (tp :: k). f tp -> a
f
zipWithM :: Applicative m
=> (forall tp . f tp -> g tp -> m (h tp))
-> Assignment f c
-> Assignment g c
-> m (Assignment h c)
zipWithM :: forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: k -> *)
(c :: Ctx k).
Applicative m =>
(forall (tp :: k). f tp -> g tp -> m (h tp))
-> Assignment f c -> Assignment g c -> m (Assignment h c)
zipWithM forall (tp :: k). f tp -> g tp -> m (h tp)
f Assignment f c
x Assignment g c
y = Assignment f c -> Assignment g c -> m (Assignment h c)
go Assignment f c
x Assignment g c
y
where go :: Assignment f c -> Assignment g c -> m (Assignment h c)
go Assignment f c
AssignmentEmpty Assignment g c
Assignment g 'EmptyCtx
AssignmentEmpty = Assignment h 'EmptyCtx -> m (Assignment h 'EmptyCtx)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Assignment h 'EmptyCtx
forall {k} (f :: k -> *). Assignment f EmptyCtx
AssignmentEmpty
go (AssignmentExtend Assignment f ctx
asgn1 f tp
x1) (AssignmentExtend Assignment g ctx
asgn2 g tp
x2) =
Assignment h ctx -> h tp -> Assignment h (ctx '::> tp)
forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
Assignment f n -> f tp -> Assignment f (n ::> tp)
AssignmentExtend (Assignment h ctx -> h tp -> Assignment h (ctx '::> tp))
-> m (Assignment h ctx) -> m (h tp -> Assignment h (ctx '::> tp))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((forall (tp :: k). f tp -> g tp -> m (h tp))
-> Assignment f ctx -> Assignment g ctx -> m (Assignment h ctx)
forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: k -> *)
(c :: Ctx k).
Applicative m =>
(forall (tp :: k). f tp -> g tp -> m (h tp))
-> Assignment f c -> Assignment g c -> m (Assignment h c)
zipWithM f tp -> g tp -> m (h tp)
forall (tp :: k). f tp -> g tp -> m (h tp)
f Assignment f ctx
asgn1 Assignment g ctx
Assignment g ctx
asgn2) m (h tp -> Assignment h (ctx '::> tp))
-> m (h tp) -> m (Assignment h (ctx '::> tp))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (f tp -> g tp -> m (h tp)
forall (tp :: k). f tp -> g tp -> m (h tp)
f f tp
x1 g tp
g tp
x2)
zipWith :: (forall x . f x -> g x -> h x)
-> Assignment f a
-> Assignment g a
-> Assignment h a
zipWith :: forall {k} (f :: k -> *) (g :: k -> *) (h :: k -> *) (a :: Ctx k).
(forall (x :: k). f x -> g x -> h x)
-> Assignment f a -> Assignment g a -> Assignment h a
zipWith forall (x :: k). f x -> g x -> h x
f = \Assignment f a
x Assignment g a
y -> Identity (Assignment h a) -> Assignment h a
forall a. Identity a -> a
runIdentity (Identity (Assignment h a) -> Assignment h a)
-> Identity (Assignment h a) -> Assignment h a
forall a b. (a -> b) -> a -> b
$ (forall (tp :: k). f tp -> g tp -> Identity (h tp))
-> Assignment f a -> Assignment g a -> Identity (Assignment h a)
forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: k -> *)
(c :: Ctx k).
Applicative m =>
(forall (tp :: k). f tp -> g tp -> m (h tp))
-> Assignment f c -> Assignment g c -> m (Assignment h c)
zipWithM (\f tp
u g tp
v -> h tp -> Identity (h tp)
forall a. a -> Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (f tp -> g tp -> h tp
forall (x :: k). f x -> g x -> h x
f f tp
u g tp
v)) Assignment f a
x Assignment g a
y
{-# INLINE zipWith #-}
traverseWithIndex :: Applicative m
=> (forall tp . Index ctx tp -> f tp -> m (g tp))
-> Assignment f ctx
-> m (Assignment g ctx)
traverseWithIndex :: forall {k} (m :: * -> *) (ctx :: Ctx k) (f :: k -> *)
(g :: k -> *).
Applicative m =>
(forall (tp :: k). Index ctx tp -> f tp -> m (g tp))
-> Assignment f ctx -> m (Assignment g ctx)
traverseWithIndex forall (tp :: k). Index ctx tp -> f tp -> m (g tp)
f Assignment f ctx
a = Size ctx
-> (forall {tp :: k}. Index ctx tp -> m (g tp))
-> m (Assignment g ctx)
forall {k} (ctx :: Ctx k) (m :: * -> *) (f :: k -> *).
Applicative m =>
Size ctx
-> (forall (tp :: k). Index ctx tp -> m (f tp))
-> m (Assignment f ctx)
generateM (Assignment f ctx -> Size ctx
forall {k} (f :: k -> *) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
size Assignment f ctx
a) ((forall {tp :: k}. Index ctx tp -> m (g tp))
-> m (Assignment g ctx))
-> (forall {tp :: k}. Index ctx tp -> m (g tp))
-> m (Assignment g ctx)
forall a b. (a -> b) -> a -> b
$ \Index ctx tp
i -> Index ctx tp -> f tp -> m (g tp)
forall (tp :: k). Index ctx tp -> f tp -> m (g tp)
f Index ctx tp
i (Assignment f ctx
a Assignment f ctx -> Index ctx tp -> f tp
forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
! Index ctx tp
i)
(<++>) :: Assignment f x -> Assignment f y -> Assignment f (x <+> y)
Assignment f x
x <++> :: forall {k} (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
Assignment f x -> Assignment f y -> Assignment f (x <+> y)
<++> Assignment f y
AssignmentEmpty = Assignment f x
Assignment f (x <+> y)
x
Assignment f x
x <++> AssignmentExtend Assignment f ctx
y f tp
t = Assignment f (x <+> ctx)
-> f tp -> Assignment f ((x <+> ctx) ::> tp)
forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
Assignment f n -> f tp -> Assignment f (n ::> tp)
AssignmentExtend (Assignment f x
x Assignment f x -> Assignment f ctx -> Assignment f (x <+> ctx)
forall {k} (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
Assignment f x -> Assignment f y -> Assignment f (x <+> y)
<++> Assignment f ctx
y) f tp
t
instance (KnownRepr (Assignment f) ctx, KnownRepr f bt)
=> KnownRepr (Assignment f) (ctx ::> bt) where
knownRepr :: Assignment f (ctx ::> bt)
knownRepr = Assignment f ctx
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr Assignment f ctx -> f bt -> Assignment f (ctx ::> bt)
forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
Assignment f n -> f tp -> Assignment f (n ::> tp)
`extend` f bt
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
instance KnownRepr (Assignment f) EmptyCtx where
knownRepr :: Assignment f EmptyCtx
knownRepr = Assignment f EmptyCtx
forall {k} (f :: k -> *). Assignment f EmptyCtx
empty
data MyNat where
MyZ :: MyNat
MyS :: MyNat -> MyNat
type MyZ = 'MyZ
type MyS = 'MyS
data MyNatRepr :: MyNat -> Type where
MyZR :: MyNatRepr MyZ
MySR :: MyNatRepr n -> MyNatRepr (MyS n)
type family StrongCtxUpdate (n::MyNat) (ctx::Ctx k) (z::k) :: Ctx k where
StrongCtxUpdate n EmptyCtx z = EmptyCtx
StrongCtxUpdate MyZ (ctx::>x) z = ctx ::> z
StrongCtxUpdate (MyS n) (ctx::>x) z = (StrongCtxUpdate n ctx z) ::> x
type family MyNatLookup (n::MyNat) (ctx::Ctx k) (f::k -> Type) :: Type where
MyNatLookup n EmptyCtx f = ()
MyNatLookup MyZ (ctx::>x) f = f x
MyNatLookup (MyS n) (ctx::>x) f = MyNatLookup n ctx f
mynat_lookup :: MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup :: forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr n
_ Assignment f ctx
AssignmentEmpty = ()
mynat_lookup MyNatRepr n
MyZR (AssignmentExtend Assignment f ctx
_ f tp
x) = f tp
MyNatLookup n ctx f
x
mynat_lookup (MySR MyNatRepr n
n) (AssignmentExtend Assignment f ctx
asgn f tp
_) = MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr n
n Assignment f ctx
asgn
strong_ctx_update :: MyNatRepr n -> Assignment f ctx -> f tp -> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update :: forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr n
_ Assignment f ctx
AssignmentEmpty f tp
_ = Assignment f 'EmptyCtx
Assignment f (StrongCtxUpdate n ctx tp)
forall {k} (f :: k -> *). Assignment f EmptyCtx
AssignmentEmpty
strong_ctx_update MyNatRepr n
MyZR (AssignmentExtend Assignment f ctx
asgn f tp
_) f tp
z = Assignment f ctx -> f tp -> Assignment f (ctx ::> tp)
forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
Assignment f n -> f tp -> Assignment f (n ::> tp)
AssignmentExtend Assignment f ctx
asgn f tp
z
strong_ctx_update (MySR MyNatRepr n
n) (AssignmentExtend Assignment f ctx
asgn f tp
x) f tp
z = Assignment f (StrongCtxUpdate n ctx tp)
-> f tp -> Assignment f (StrongCtxUpdate n ctx tp ::> tp)
forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
Assignment f n -> f tp -> Assignment f (n ::> tp)
AssignmentExtend (MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr n
n Assignment f ctx
asgn f tp
z) f tp
x
type Assignment1 f x1 = Assignment f ('EmptyCtx '::> x1)
instance Lens.Field1 (Assignment1 f t) (Assignment1 f u) (f t) (f u) where
_1 :: Lens (Assignment1 f t) (Assignment1 f u) (f t) (f u)
_1 = (Assignment1 f t -> f t)
-> (Assignment1 f t -> f u -> Assignment1 f u)
-> Lens (Assignment1 f t) (Assignment1 f u) (f t) (f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr 'MyZ
-> Assignment1 f t -> MyNatLookup 'MyZ ('EmptyCtx '::> t) f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr 'MyZ
n) (MyNatRepr 'MyZ
-> Assignment1 f t
-> f u
-> Assignment f (StrongCtxUpdate 'MyZ ('EmptyCtx '::> t) u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr 'MyZ
n)
where n :: MyNatRepr 'MyZ
n = MyNatRepr 'MyZ
MyZR
type Assignment2 f x1 x2
= Assignment f ('EmptyCtx '::> x1 '::> x2)
instance Lens.Field1 (Assignment2 f t x2) (Assignment2 f u x2) (f t) (f u) where
_1 :: Lens (Assignment2 f t x2) (Assignment2 f u x2) (f t) (f u)
_1 = (Assignment2 f t x2 -> f t)
-> (Assignment2 f t x2 -> f u -> Assignment2 f u x2)
-> Lens (Assignment2 f t x2) (Assignment2 f u x2) (f t) (f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr (MyS 'MyZ)
-> Assignment2 f t x2
-> MyNatLookup (MyS 'MyZ) (('EmptyCtx '::> t) '::> x2) f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS 'MyZ)
n) (MyNatRepr (MyS 'MyZ)
-> Assignment2 f t x2
-> f u
-> Assignment
f (StrongCtxUpdate (MyS 'MyZ) (('EmptyCtx '::> t) '::> x2) u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS 'MyZ)
n)
where n :: MyNatRepr (MyS 'MyZ)
n = MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
-> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR
instance Lens.Field2 (Assignment2 f x1 t) (Assignment2 f x1 u) (f t) (f u) where
_2 :: Lens (Assignment2 f x1 t) (Assignment2 f x1 u) (f t) (f u)
_2 = (Assignment2 f x1 t -> f t)
-> (Assignment2 f x1 t -> f u -> Assignment2 f x1 u)
-> Lens (Assignment2 f x1 t) (Assignment2 f x1 u) (f t) (f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr 'MyZ
-> Assignment2 f x1 t
-> MyNatLookup 'MyZ (('EmptyCtx '::> x1) '::> t) f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr 'MyZ
n) (MyNatRepr 'MyZ
-> Assignment2 f x1 t
-> f u
-> Assignment
f (StrongCtxUpdate 'MyZ (('EmptyCtx '::> x1) '::> t) u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr 'MyZ
n)
where n :: MyNatRepr 'MyZ
n = MyNatRepr 'MyZ
MyZR
type Assignment3 f x1 x2 x3
= Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3)
instance Lens.Field1 (Assignment3 f t x2 x3)
(Assignment3 f u x2 x3)
(f t)
(f u) where
_1 :: Lens (Assignment3 f t x2 x3) (Assignment3 f u x2 x3) (f t) (f u)
_1 = (Assignment3 f t x2 x3 -> f t)
-> (Assignment3 f t x2 x3 -> f u -> Assignment3 f u x2 x3)
-> Lens (Assignment3 f t x2 x3) (Assignment3 f u x2 x3) (f t) (f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr (MyS (MyS 'MyZ))
-> Assignment3 f t x2 x3
-> MyNatLookup
(MyS (MyS 'MyZ)) ((('EmptyCtx '::> t) '::> x2) '::> x3) f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS 'MyZ))
n) (MyNatRepr (MyS (MyS 'MyZ))
-> Assignment3 f t x2 x3
-> f u
-> Assignment
f
(StrongCtxUpdate
(MyS (MyS 'MyZ)) ((('EmptyCtx '::> t) '::> x2) '::> x3) u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS 'MyZ))
n)
where n :: MyNatRepr (MyS (MyS 'MyZ))
n = MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
-> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR
instance Lens.Field2 (Assignment3 f x1 t x3)
(Assignment3 f x1 u x3)
(f t)
(f u) where
_2 :: Lens (Assignment3 f x1 t x3) (Assignment3 f x1 u x3) (f t) (f u)
_2 = (Assignment3 f x1 t x3 -> f t)
-> (Assignment3 f x1 t x3 -> f u -> Assignment3 f x1 u x3)
-> Lens (Assignment3 f x1 t x3) (Assignment3 f x1 u x3) (f t) (f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr (MyS 'MyZ)
-> Assignment3 f x1 t x3
-> MyNatLookup (MyS 'MyZ) ((('EmptyCtx '::> x1) '::> t) '::> x3) f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS 'MyZ)
n) (MyNatRepr (MyS 'MyZ)
-> Assignment3 f x1 t x3
-> f u
-> Assignment
f
(StrongCtxUpdate
(MyS 'MyZ) ((('EmptyCtx '::> x1) '::> t) '::> x3) u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS 'MyZ)
n)
where n :: MyNatRepr (MyS 'MyZ)
n = MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
-> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR
instance Lens.Field3 (Assignment3 f x1 x2 t)
(Assignment3 f x1 x2 u)
(f t)
(f u) where
_3 :: Lens (Assignment3 f x1 x2 t) (Assignment3 f x1 x2 u) (f t) (f u)
_3 = (Assignment3 f x1 x2 t -> f t)
-> (Assignment3 f x1 x2 t -> f u -> Assignment3 f x1 x2 u)
-> Lens (Assignment3 f x1 x2 t) (Assignment3 f x1 x2 u) (f t) (f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr 'MyZ
-> Assignment3 f x1 x2 t
-> MyNatLookup 'MyZ ((('EmptyCtx '::> x1) '::> x2) '::> t) f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr 'MyZ
n) (MyNatRepr 'MyZ
-> Assignment3 f x1 x2 t
-> f u
-> Assignment
f (StrongCtxUpdate 'MyZ ((('EmptyCtx '::> x1) '::> x2) '::> t) u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr 'MyZ
n)
where n :: MyNatRepr 'MyZ
n = MyNatRepr 'MyZ
MyZR
type Assignment4 f x1 x2 x3 x4
= Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4)
instance Lens.Field1 (Assignment4 f t x2 x3 x4)
(Assignment4 f u x2 x3 x4)
(f t)
(f u) where
_1 :: Lens
(Assignment4 f t x2 x3 x4) (Assignment4 f u x2 x3 x4) (f t) (f u)
_1 = (Assignment4 f t x2 x3 x4 -> f t)
-> (Assignment4 f t x2 x3 x4 -> f u -> Assignment4 f u x2 x3 x4)
-> Lens
(Assignment4 f t x2 x3 x4) (Assignment4 f u x2 x3 x4) (f t) (f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> Assignment4 f t x2 x3 x4
-> MyNatLookup
(MyS (MyS (MyS 'MyZ)))
(((('EmptyCtx '::> t) '::> x2) '::> x3) '::> x4)
f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS 'MyZ)))
n) (MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> Assignment4 f t x2 x3 x4
-> f u
-> Assignment
f
(StrongCtxUpdate
(MyS (MyS (MyS 'MyZ)))
(((('EmptyCtx '::> t) '::> x2) '::> x3) '::> x4)
u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS 'MyZ)))
n)
where n :: MyNatRepr (MyS (MyS (MyS 'MyZ)))
n = MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
-> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR
instance Lens.Field2 (Assignment4 f x1 t x3 x4)
(Assignment4 f x1 u x3 x4)
(f t)
(f u) where
_2 :: Lens
(Assignment4 f x1 t x3 x4) (Assignment4 f x1 u x3 x4) (f t) (f u)
_2 = (Assignment4 f x1 t x3 x4 -> f t)
-> (Assignment4 f x1 t x3 x4 -> f u -> Assignment4 f x1 u x3 x4)
-> Lens
(Assignment4 f x1 t x3 x4) (Assignment4 f x1 u x3 x4) (f t) (f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr (MyS (MyS 'MyZ))
-> Assignment4 f x1 t x3 x4
-> MyNatLookup
(MyS (MyS 'MyZ)) (((('EmptyCtx '::> x1) '::> t) '::> x3) '::> x4) f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS 'MyZ))
n) (MyNatRepr (MyS (MyS 'MyZ))
-> Assignment4 f x1 t x3 x4
-> f u
-> Assignment
f
(StrongCtxUpdate
(MyS (MyS 'MyZ))
(((('EmptyCtx '::> x1) '::> t) '::> x3) '::> x4)
u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS 'MyZ))
n)
where n :: MyNatRepr (MyS (MyS 'MyZ))
n = MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
-> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR
instance Lens.Field3 (Assignment4 f x1 x2 t x4)
(Assignment4 f x1 x2 u x4)
(f t)
(f u) where
_3 :: Lens
(Assignment4 f x1 x2 t x4) (Assignment4 f x1 x2 u x4) (f t) (f u)
_3 = (Assignment4 f x1 x2 t x4 -> f t)
-> (Assignment4 f x1 x2 t x4 -> f u -> Assignment4 f x1 x2 u x4)
-> Lens
(Assignment4 f x1 x2 t x4) (Assignment4 f x1 x2 u x4) (f t) (f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr (MyS 'MyZ)
-> Assignment4 f x1 x2 t x4
-> MyNatLookup
(MyS 'MyZ) (((('EmptyCtx '::> x1) '::> x2) '::> t) '::> x4) f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS 'MyZ)
n) (MyNatRepr (MyS 'MyZ)
-> Assignment4 f x1 x2 t x4
-> f u
-> Assignment
f
(StrongCtxUpdate
(MyS 'MyZ) (((('EmptyCtx '::> x1) '::> x2) '::> t) '::> x4) u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS 'MyZ)
n)
where n :: MyNatRepr (MyS 'MyZ)
n = MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
-> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR
instance Lens.Field4 (Assignment4 f x1 x2 x3 t)
(Assignment4 f x1 x2 x3 u)
(f t)
(f u) where
_4 :: Lens
(Assignment4 f x1 x2 x3 t) (Assignment4 f x1 x2 x3 u) (f t) (f u)
_4 = (Assignment4 f x1 x2 x3 t -> f t)
-> (Assignment4 f x1 x2 x3 t -> f u -> Assignment4 f x1 x2 x3 u)
-> Lens
(Assignment4 f x1 x2 x3 t) (Assignment4 f x1 x2 x3 u) (f t) (f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr 'MyZ
-> Assignment4 f x1 x2 x3 t
-> MyNatLookup
'MyZ (((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> t) f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr 'MyZ
n) (MyNatRepr 'MyZ
-> Assignment4 f x1 x2 x3 t
-> f u
-> Assignment
f
(StrongCtxUpdate
'MyZ (((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> t) u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr 'MyZ
n)
where n :: MyNatRepr 'MyZ
n = MyNatRepr 'MyZ
MyZR
type Assignment5 f x1 x2 x3 x4 x5
= Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4 '::> x5)
instance Lens.Field1 (Assignment5 f t x2 x3 x4 x5)
(Assignment5 f u x2 x3 x4 x5)
(f t)
(f u) where
_1 :: Lens
(Assignment5 f t x2 x3 x4 x5)
(Assignment5 f u x2 x3 x4 x5)
(f t)
(f u)
_1 = (Assignment5 f t x2 x3 x4 x5 -> f t)
-> (Assignment5 f t x2 x3 x4 x5
-> f u -> Assignment5 f u x2 x3 x4 x5)
-> Lens
(Assignment5 f t x2 x3 x4 x5)
(Assignment5 f u x2 x3 x4 x5)
(f t)
(f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> Assignment5 f t x2 x3 x4 x5
-> MyNatLookup
(MyS (MyS (MyS (MyS 'MyZ))))
((((('EmptyCtx '::> t) '::> x2) '::> x3) '::> x4) '::> x5)
f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
n) (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> Assignment5 f t x2 x3 x4 x5
-> f u
-> Assignment
f
(StrongCtxUpdate
(MyS (MyS (MyS (MyS 'MyZ))))
((((('EmptyCtx '::> t) '::> x2) '::> x3) '::> x4) '::> x5)
u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
n)
where n :: MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
n = MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ)))))
-> MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
-> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR
instance Lens.Field2 (Assignment5 f x1 t x3 x4 x5)
(Assignment5 f x1 u x3 x4 x5)
(f t)
(f u) where
_2 :: Lens
(Assignment5 f x1 t x3 x4 x5)
(Assignment5 f x1 u x3 x4 x5)
(f t)
(f u)
_2 = (Assignment5 f x1 t x3 x4 x5 -> f t)
-> (Assignment5 f x1 t x3 x4 x5
-> f u -> Assignment5 f x1 u x3 x4 x5)
-> Lens
(Assignment5 f x1 t x3 x4 x5)
(Assignment5 f x1 u x3 x4 x5)
(f t)
(f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> Assignment5 f x1 t x3 x4 x5
-> MyNatLookup
(MyS (MyS (MyS 'MyZ)))
((((('EmptyCtx '::> x1) '::> t) '::> x3) '::> x4) '::> x5)
f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS 'MyZ)))
n) (MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> Assignment5 f x1 t x3 x4 x5
-> f u
-> Assignment
f
(StrongCtxUpdate
(MyS (MyS (MyS 'MyZ)))
((((('EmptyCtx '::> x1) '::> t) '::> x3) '::> x4) '::> x5)
u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS 'MyZ)))
n)
where n :: MyNatRepr (MyS (MyS (MyS 'MyZ)))
n = MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
-> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR
instance Lens.Field3 (Assignment5 f x1 x2 t x4 x5)
(Assignment5 f x1 x2 u x4 x5)
(f t)
(f u) where
_3 :: Lens
(Assignment5 f x1 x2 t x4 x5)
(Assignment5 f x1 x2 u x4 x5)
(f t)
(f u)
_3 = (Assignment5 f x1 x2 t x4 x5 -> f t)
-> (Assignment5 f x1 x2 t x4 x5
-> f u -> Assignment5 f x1 x2 u x4 x5)
-> Lens
(Assignment5 f x1 x2 t x4 x5)
(Assignment5 f x1 x2 u x4 x5)
(f t)
(f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr (MyS (MyS 'MyZ))
-> Assignment5 f x1 x2 t x4 x5
-> MyNatLookup
(MyS (MyS 'MyZ))
((((('EmptyCtx '::> x1) '::> x2) '::> t) '::> x4) '::> x5)
f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS 'MyZ))
n) (MyNatRepr (MyS (MyS 'MyZ))
-> Assignment5 f x1 x2 t x4 x5
-> f u
-> Assignment
f
(StrongCtxUpdate
(MyS (MyS 'MyZ))
((((('EmptyCtx '::> x1) '::> x2) '::> t) '::> x4) '::> x5)
u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS 'MyZ))
n)
where n :: MyNatRepr (MyS (MyS 'MyZ))
n = MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
-> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR
instance Lens.Field4 (Assignment5 f x1 x2 x3 t x5)
(Assignment5 f x1 x2 x3 u x5)
(f t)
(f u) where
_4 :: Lens
(Assignment5 f x1 x2 x3 t x5)
(Assignment5 f x1 x2 x3 u x5)
(f t)
(f u)
_4 = (Assignment5 f x1 x2 x3 t x5 -> f t)
-> (Assignment5 f x1 x2 x3 t x5
-> f u -> Assignment5 f x1 x2 x3 u x5)
-> Lens
(Assignment5 f x1 x2 x3 t x5)
(Assignment5 f x1 x2 x3 u x5)
(f t)
(f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr (MyS 'MyZ)
-> Assignment5 f x1 x2 x3 t x5
-> MyNatLookup
(MyS 'MyZ)
((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> t) '::> x5)
f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS 'MyZ)
n) (MyNatRepr (MyS 'MyZ)
-> Assignment5 f x1 x2 x3 t x5
-> f u
-> Assignment
f
(StrongCtxUpdate
(MyS 'MyZ)
((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> t) '::> x5)
u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS 'MyZ)
n)
where n :: MyNatRepr (MyS 'MyZ)
n = MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
-> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR
instance Lens.Field5 (Assignment5 f x1 x2 x3 x4 t)
(Assignment5 f x1 x2 x3 x4 u)
(f t)
(f u) where
_5 :: Lens
(Assignment5 f x1 x2 x3 x4 t)
(Assignment5 f x1 x2 x3 x4 u)
(f t)
(f u)
_5 = (Assignment5 f x1 x2 x3 x4 t -> f t)
-> (Assignment5 f x1 x2 x3 x4 t
-> f u -> Assignment5 f x1 x2 x3 x4 u)
-> Lens
(Assignment5 f x1 x2 x3 x4 t)
(Assignment5 f x1 x2 x3 x4 u)
(f t)
(f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr 'MyZ
-> Assignment5 f x1 x2 x3 x4 t
-> MyNatLookup
'MyZ ((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> t) f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr 'MyZ
n) (MyNatRepr 'MyZ
-> Assignment5 f x1 x2 x3 x4 t
-> f u
-> Assignment
f
(StrongCtxUpdate
'MyZ ((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> t) u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr 'MyZ
n)
where n :: MyNatRepr 'MyZ
n = MyNatRepr 'MyZ
MyZR
type Assignment6 f x1 x2 x3 x4 x5 x6
= Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4 '::> x5 '::> x6)
instance Lens.Field1 (Assignment6 f t x2 x3 x4 x5 x6)
(Assignment6 f u x2 x3 x4 x5 x6)
(f t)
(f u) where
_1 :: Lens
(Assignment6 f t x2 x3 x4 x5 x6)
(Assignment6 f u x2 x3 x4 x5 x6)
(f t)
(f u)
_1 = (Assignment6 f t x2 x3 x4 x5 x6 -> f t)
-> (Assignment6 f t x2 x3 x4 x5 x6
-> f u -> Assignment6 f u x2 x3 x4 x5 x6)
-> Lens
(Assignment6 f t x2 x3 x4 x5 x6)
(Assignment6 f u x2 x3 x4 x5 x6)
(f t)
(f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
-> Assignment6 f t x2 x3 x4 x5 x6
-> MyNatLookup
(MyS (MyS (MyS (MyS (MyS 'MyZ)))))
(((((('EmptyCtx '::> t) '::> x2) '::> x3) '::> x4) '::> x5)
'::> x6)
f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
n) (MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
-> Assignment6 f t x2 x3 x4 x5 x6
-> f u
-> Assignment
f
(StrongCtxUpdate
(MyS (MyS (MyS (MyS (MyS 'MyZ)))))
(((((('EmptyCtx '::> t) '::> x2) '::> x3) '::> x4) '::> x5)
'::> x6)
u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
n)
where n :: MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
n = MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ)))))
-> MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
-> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR
instance Lens.Field2 (Assignment6 f x1 t x3 x4 x5 x6)
(Assignment6 f x1 u x3 x4 x5 x6)
(f t)
(f u) where
_2 :: Lens
(Assignment6 f x1 t x3 x4 x5 x6)
(Assignment6 f x1 u x3 x4 x5 x6)
(f t)
(f u)
_2 = (Assignment6 f x1 t x3 x4 x5 x6 -> f t)
-> (Assignment6 f x1 t x3 x4 x5 x6
-> f u -> Assignment6 f x1 u x3 x4 x5 x6)
-> Lens
(Assignment6 f x1 t x3 x4 x5 x6)
(Assignment6 f x1 u x3 x4 x5 x6)
(f t)
(f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> Assignment6 f x1 t x3 x4 x5 x6
-> MyNatLookup
(MyS (MyS (MyS (MyS 'MyZ))))
(((((('EmptyCtx '::> x1) '::> t) '::> x3) '::> x4) '::> x5)
'::> x6)
f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
n) (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> Assignment6 f x1 t x3 x4 x5 x6
-> f u
-> Assignment
f
(StrongCtxUpdate
(MyS (MyS (MyS (MyS 'MyZ))))
(((((('EmptyCtx '::> x1) '::> t) '::> x3) '::> x4) '::> x5)
'::> x6)
u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
n)
where n :: MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
n = MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ)))))
-> MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
-> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR
instance Lens.Field3 (Assignment6 f x1 x2 t x4 x5 x6)
(Assignment6 f x1 x2 u x4 x5 x6)
(f t)
(f u) where
_3 :: Lens
(Assignment6 f x1 x2 t x4 x5 x6)
(Assignment6 f x1 x2 u x4 x5 x6)
(f t)
(f u)
_3 = (Assignment6 f x1 x2 t x4 x5 x6 -> f t)
-> (Assignment6 f x1 x2 t x4 x5 x6
-> f u -> Assignment6 f x1 x2 u x4 x5 x6)
-> Lens
(Assignment6 f x1 x2 t x4 x5 x6)
(Assignment6 f x1 x2 u x4 x5 x6)
(f t)
(f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> Assignment6 f x1 x2 t x4 x5 x6
-> MyNatLookup
(MyS (MyS (MyS 'MyZ)))
(((((('EmptyCtx '::> x1) '::> x2) '::> t) '::> x4) '::> x5)
'::> x6)
f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS 'MyZ)))
n) (MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> Assignment6 f x1 x2 t x4 x5 x6
-> f u
-> Assignment
f
(StrongCtxUpdate
(MyS (MyS (MyS 'MyZ)))
(((((('EmptyCtx '::> x1) '::> x2) '::> t) '::> x4) '::> x5)
'::> x6)
u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS 'MyZ)))
n)
where n :: MyNatRepr (MyS (MyS (MyS 'MyZ)))
n = MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
-> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR
instance Lens.Field4 (Assignment6 f x1 x2 x3 t x5 x6)
(Assignment6 f x1 x2 x3 u x5 x6)
(f t)
(f u) where
_4 :: Lens
(Assignment6 f x1 x2 x3 t x5 x6)
(Assignment6 f x1 x2 x3 u x5 x6)
(f t)
(f u)
_4 = (Assignment6 f x1 x2 x3 t x5 x6 -> f t)
-> (Assignment6 f x1 x2 x3 t x5 x6
-> f u -> Assignment6 f x1 x2 x3 u x5 x6)
-> Lens
(Assignment6 f x1 x2 x3 t x5 x6)
(Assignment6 f x1 x2 x3 u x5 x6)
(f t)
(f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr (MyS (MyS 'MyZ))
-> Assignment6 f x1 x2 x3 t x5 x6
-> MyNatLookup
(MyS (MyS 'MyZ))
(((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> t) '::> x5)
'::> x6)
f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS 'MyZ))
n) (MyNatRepr (MyS (MyS 'MyZ))
-> Assignment6 f x1 x2 x3 t x5 x6
-> f u
-> Assignment
f
(StrongCtxUpdate
(MyS (MyS 'MyZ))
(((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> t) '::> x5)
'::> x6)
u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS 'MyZ))
n)
where n :: MyNatRepr (MyS (MyS 'MyZ))
n = MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
-> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR
instance Lens.Field5 (Assignment6 f x1 x2 x3 x4 t x6)
(Assignment6 f x1 x2 x3 x4 u x6)
(f t)
(f u) where
_5 :: Lens
(Assignment6 f x1 x2 x3 x4 t x6)
(Assignment6 f x1 x2 x3 x4 u x6)
(f t)
(f u)
_5 = (Assignment6 f x1 x2 x3 x4 t x6 -> f t)
-> (Assignment6 f x1 x2 x3 x4 t x6
-> f u -> Assignment6 f x1 x2 x3 x4 u x6)
-> Lens
(Assignment6 f x1 x2 x3 x4 t x6)
(Assignment6 f x1 x2 x3 x4 u x6)
(f t)
(f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr (MyS 'MyZ)
-> Assignment6 f x1 x2 x3 x4 t x6
-> MyNatLookup
(MyS 'MyZ)
(((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> t)
'::> x6)
f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS 'MyZ)
n) (MyNatRepr (MyS 'MyZ)
-> Assignment6 f x1 x2 x3 x4 t x6
-> f u
-> Assignment
f
(StrongCtxUpdate
(MyS 'MyZ)
(((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> t)
'::> x6)
u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS 'MyZ)
n)
where n :: MyNatRepr (MyS 'MyZ)
n = MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
-> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR
instance Lens.Field6 (Assignment6 f x1 x2 x3 x4 x5 t)
(Assignment6 f x1 x2 x3 x4 x5 u)
(f t)
(f u) where
_6 :: Lens
(Assignment6 f x1 x2 x3 x4 x5 t)
(Assignment6 f x1 x2 x3 x4 x5 u)
(f t)
(f u)
_6 = (Assignment6 f x1 x2 x3 x4 x5 t -> f t)
-> (Assignment6 f x1 x2 x3 x4 x5 t
-> f u -> Assignment6 f x1 x2 x3 x4 x5 u)
-> Lens
(Assignment6 f x1 x2 x3 x4 x5 t)
(Assignment6 f x1 x2 x3 x4 x5 u)
(f t)
(f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr 'MyZ
-> Assignment6 f x1 x2 x3 x4 x5 t
-> MyNatLookup
'MyZ
(((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
'::> t)
f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr 'MyZ
n) (MyNatRepr 'MyZ
-> Assignment6 f x1 x2 x3 x4 x5 t
-> f u
-> Assignment
f
(StrongCtxUpdate
'MyZ
(((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
'::> t)
u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr 'MyZ
n)
where n :: MyNatRepr 'MyZ
n = MyNatRepr 'MyZ
MyZR
type Assignment7 f x1 x2 x3 x4 x5 x6 x7
= Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4 '::> x5 '::> x6 '::> x7)
instance Lens.Field1 (Assignment7 f t x2 x3 x4 x5 x6 x7)
(Assignment7 f u x2 x3 x4 x5 x6 x7)
(f t)
(f u) where
_1 :: Lens
(Assignment7 f t x2 x3 x4 x5 x6 x7)
(Assignment7 f u x2 x3 x4 x5 x6 x7)
(f t)
(f u)
_1 = (Assignment7 f t x2 x3 x4 x5 x6 x7 -> f t)
-> (Assignment7 f t x2 x3 x4 x5 x6 x7
-> f u -> Assignment7 f u x2 x3 x4 x5 x6 x7)
-> Lens
(Assignment7 f t x2 x3 x4 x5 x6 x7)
(Assignment7 f u x2 x3 x4 x5 x6 x7)
(f t)
(f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
-> Assignment7 f t x2 x3 x4 x5 x6 x7
-> MyNatLookup
(MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
((((((('EmptyCtx '::> t) '::> x2) '::> x3) '::> x4) '::> x5)
'::> x6)
'::> x7)
f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
n) (MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
-> Assignment7 f t x2 x3 x4 x5 x6 x7
-> f u
-> Assignment
f
(StrongCtxUpdate
(MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
((((((('EmptyCtx '::> t) '::> x2) '::> x3) '::> x4) '::> x5)
'::> x6)
'::> x7)
u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
n)
where n :: MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
n = MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ)))))
-> MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
-> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR
instance Lens.Field2 (Assignment7 f x1 t x3 x4 x5 x6 x7)
(Assignment7 f x1 u x3 x4 x5 x6 x7)
(f t)
(f u) where
_2 :: Lens
(Assignment7 f x1 t x3 x4 x5 x6 x7)
(Assignment7 f x1 u x3 x4 x5 x6 x7)
(f t)
(f u)
_2 = (Assignment7 f x1 t x3 x4 x5 x6 x7 -> f t)
-> (Assignment7 f x1 t x3 x4 x5 x6 x7
-> f u -> Assignment7 f x1 u x3 x4 x5 x6 x7)
-> Lens
(Assignment7 f x1 t x3 x4 x5 x6 x7)
(Assignment7 f x1 u x3 x4 x5 x6 x7)
(f t)
(f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
-> Assignment7 f x1 t x3 x4 x5 x6 x7
-> MyNatLookup
(MyS (MyS (MyS (MyS (MyS 'MyZ)))))
((((((('EmptyCtx '::> x1) '::> t) '::> x3) '::> x4) '::> x5)
'::> x6)
'::> x7)
f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
n) (MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
-> Assignment7 f x1 t x3 x4 x5 x6 x7
-> f u
-> Assignment
f
(StrongCtxUpdate
(MyS (MyS (MyS (MyS (MyS 'MyZ)))))
((((((('EmptyCtx '::> x1) '::> t) '::> x3) '::> x4) '::> x5)
'::> x6)
'::> x7)
u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
n)
where n :: MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
n = MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ)))))
-> MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
-> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR
instance Lens.Field3 (Assignment7 f x1 x2 t x4 x5 x6 x7)
(Assignment7 f x1 x2 u x4 x5 x6 x7)
(f t)
(f u) where
_3 :: Lens
(Assignment7 f x1 x2 t x4 x5 x6 x7)
(Assignment7 f x1 x2 u x4 x5 x6 x7)
(f t)
(f u)
_3 = (Assignment7 f x1 x2 t x4 x5 x6 x7 -> f t)
-> (Assignment7 f x1 x2 t x4 x5 x6 x7
-> f u -> Assignment7 f x1 x2 u x4 x5 x6 x7)
-> Lens
(Assignment7 f x1 x2 t x4 x5 x6 x7)
(Assignment7 f x1 x2 u x4 x5 x6 x7)
(f t)
(f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> Assignment7 f x1 x2 t x4 x5 x6 x7
-> MyNatLookup
(MyS (MyS (MyS (MyS 'MyZ))))
((((((('EmptyCtx '::> x1) '::> x2) '::> t) '::> x4) '::> x5)
'::> x6)
'::> x7)
f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
n) (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> Assignment7 f x1 x2 t x4 x5 x6 x7
-> f u
-> Assignment
f
(StrongCtxUpdate
(MyS (MyS (MyS (MyS 'MyZ))))
((((((('EmptyCtx '::> x1) '::> x2) '::> t) '::> x4) '::> x5)
'::> x6)
'::> x7)
u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
n)
where n :: MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
n = MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ)))))
-> MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
-> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR
instance Lens.Field4 (Assignment7 f x1 x2 x3 t x5 x6 x7)
(Assignment7 f x1 x2 x3 u x5 x6 x7)
(f t)
(f u) where
_4 :: Lens
(Assignment7 f x1 x2 x3 t x5 x6 x7)
(Assignment7 f x1 x2 x3 u x5 x6 x7)
(f t)
(f u)
_4 = (Assignment7 f x1 x2 x3 t x5 x6 x7 -> f t)
-> (Assignment7 f x1 x2 x3 t x5 x6 x7
-> f u -> Assignment7 f x1 x2 x3 u x5 x6 x7)
-> Lens
(Assignment7 f x1 x2 x3 t x5 x6 x7)
(Assignment7 f x1 x2 x3 u x5 x6 x7)
(f t)
(f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> Assignment7 f x1 x2 x3 t x5 x6 x7
-> MyNatLookup
(MyS (MyS (MyS 'MyZ)))
((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> t) '::> x5)
'::> x6)
'::> x7)
f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS 'MyZ)))
n) (MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> Assignment7 f x1 x2 x3 t x5 x6 x7
-> f u
-> Assignment
f
(StrongCtxUpdate
(MyS (MyS (MyS 'MyZ)))
((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> t) '::> x5)
'::> x6)
'::> x7)
u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS 'MyZ)))
n)
where n :: MyNatRepr (MyS (MyS (MyS 'MyZ)))
n = MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
-> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR
instance Lens.Field5 (Assignment7 f x1 x2 x3 x4 t x6 x7)
(Assignment7 f x1 x2 x3 x4 u x6 x7)
(f t)
(f u) where
_5 :: Lens
(Assignment7 f x1 x2 x3 x4 t x6 x7)
(Assignment7 f x1 x2 x3 x4 u x6 x7)
(f t)
(f u)
_5 = (Assignment7 f x1 x2 x3 x4 t x6 x7 -> f t)
-> (Assignment7 f x1 x2 x3 x4 t x6 x7
-> f u -> Assignment7 f x1 x2 x3 x4 u x6 x7)
-> Lens
(Assignment7 f x1 x2 x3 x4 t x6 x7)
(Assignment7 f x1 x2 x3 x4 u x6 x7)
(f t)
(f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr (MyS (MyS 'MyZ))
-> Assignment7 f x1 x2 x3 x4 t x6 x7
-> MyNatLookup
(MyS (MyS 'MyZ))
((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> t)
'::> x6)
'::> x7)
f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS 'MyZ))
n) (MyNatRepr (MyS (MyS 'MyZ))
-> Assignment7 f x1 x2 x3 x4 t x6 x7
-> f u
-> Assignment
f
(StrongCtxUpdate
(MyS (MyS 'MyZ))
((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> t)
'::> x6)
'::> x7)
u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS 'MyZ))
n)
where n :: MyNatRepr (MyS (MyS 'MyZ))
n = MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
-> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR
instance Lens.Field6 (Assignment7 f x1 x2 x3 x4 x5 t x7)
(Assignment7 f x1 x2 x3 x4 x5 u x7)
(f t)
(f u) where
_6 :: Lens
(Assignment7 f x1 x2 x3 x4 x5 t x7)
(Assignment7 f x1 x2 x3 x4 x5 u x7)
(f t)
(f u)
_6 = (Assignment7 f x1 x2 x3 x4 x5 t x7 -> f t)
-> (Assignment7 f x1 x2 x3 x4 x5 t x7
-> f u -> Assignment7 f x1 x2 x3 x4 x5 u x7)
-> Lens
(Assignment7 f x1 x2 x3 x4 x5 t x7)
(Assignment7 f x1 x2 x3 x4 x5 u x7)
(f t)
(f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr (MyS 'MyZ)
-> Assignment7 f x1 x2 x3 x4 x5 t x7
-> MyNatLookup
(MyS 'MyZ)
((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
'::> t)
'::> x7)
f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS 'MyZ)
n) (MyNatRepr (MyS 'MyZ)
-> Assignment7 f x1 x2 x3 x4 x5 t x7
-> f u
-> Assignment
f
(StrongCtxUpdate
(MyS 'MyZ)
((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
'::> t)
'::> x7)
u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS 'MyZ)
n)
where n :: MyNatRepr (MyS 'MyZ)
n = MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
-> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR
instance Lens.Field7 (Assignment7 f x1 x2 x3 x4 x5 x6 t)
(Assignment7 f x1 x2 x3 x4 x5 x6 u)
(f t)
(f u) where
_7 :: Lens
(Assignment7 f x1 x2 x3 x4 x5 x6 t)
(Assignment7 f x1 x2 x3 x4 x5 x6 u)
(f t)
(f u)
_7 = (Assignment7 f x1 x2 x3 x4 x5 x6 t -> f t)
-> (Assignment7 f x1 x2 x3 x4 x5 x6 t
-> f u -> Assignment7 f x1 x2 x3 x4 x5 x6 u)
-> Lens
(Assignment7 f x1 x2 x3 x4 x5 x6 t)
(Assignment7 f x1 x2 x3 x4 x5 x6 u)
(f t)
(f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr 'MyZ
-> Assignment7 f x1 x2 x3 x4 x5 x6 t
-> MyNatLookup
'MyZ
((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
'::> x6)
'::> t)
f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr 'MyZ
n) (MyNatRepr 'MyZ
-> Assignment7 f x1 x2 x3 x4 x5 x6 t
-> f u
-> Assignment
f
(StrongCtxUpdate
'MyZ
((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
'::> x6)
'::> t)
u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr 'MyZ
n)
where n :: MyNatRepr 'MyZ
n = MyNatRepr 'MyZ
MyZR
type Assignment8 f x1 x2 x3 x4 x5 x6 x7 x8
= Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4 '::> x5 '::> x6 '::> x7 '::> x8)
instance Lens.Field1 (Assignment8 f t x2 x3 x4 x5 x6 x7 x8)
(Assignment8 f u x2 x3 x4 x5 x6 x7 x8)
(f t)
(f u) where
_1 :: Lens
(Assignment8 f t x2 x3 x4 x5 x6 x7 x8)
(Assignment8 f u x2 x3 x4 x5 x6 x7 x8)
(f t)
(f u)
_1 = (Assignment8 f t x2 x3 x4 x5 x6 x7 x8 -> f t)
-> (Assignment8 f t x2 x3 x4 x5 x6 x7 x8
-> f u -> Assignment8 f u x2 x3 x4 x5 x6 x7 x8)
-> Lens
(Assignment8 f t x2 x3 x4 x5 x6 x7 x8)
(Assignment8 f u x2 x3 x4 x5 x6 x7 x8)
(f t)
(f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
-> Assignment8 f t x2 x3 x4 x5 x6 x7 x8
-> MyNatLookup
(MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
(((((((('EmptyCtx '::> t) '::> x2) '::> x3) '::> x4) '::> x5)
'::> x6)
'::> x7)
'::> x8)
f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
n) (MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
-> Assignment8 f t x2 x3 x4 x5 x6 x7 x8
-> f u
-> Assignment
f
(StrongCtxUpdate
(MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
(((((((('EmptyCtx '::> t) '::> x2) '::> x3) '::> x4) '::> x5)
'::> x6)
'::> x7)
'::> x8)
u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
n)
where n :: MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
n = MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ)))))
-> MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
-> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR
instance Lens.Field2 (Assignment8 f x1 t x3 x4 x5 x6 x7 x8)
(Assignment8 f x1 u x3 x4 x5 x6 x7 x8)
(f t)
(f u) where
_2 :: Lens
(Assignment8 f x1 t x3 x4 x5 x6 x7 x8)
(Assignment8 f x1 u x3 x4 x5 x6 x7 x8)
(f t)
(f u)
_2 = (Assignment8 f x1 t x3 x4 x5 x6 x7 x8 -> f t)
-> (Assignment8 f x1 t x3 x4 x5 x6 x7 x8
-> f u -> Assignment8 f x1 u x3 x4 x5 x6 x7 x8)
-> Lens
(Assignment8 f x1 t x3 x4 x5 x6 x7 x8)
(Assignment8 f x1 u x3 x4 x5 x6 x7 x8)
(f t)
(f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
-> Assignment8 f x1 t x3 x4 x5 x6 x7 x8
-> MyNatLookup
(MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
(((((((('EmptyCtx '::> x1) '::> t) '::> x3) '::> x4) '::> x5)
'::> x6)
'::> x7)
'::> x8)
f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
n) (MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
-> Assignment8 f x1 t x3 x4 x5 x6 x7 x8
-> f u
-> Assignment
f
(StrongCtxUpdate
(MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
(((((((('EmptyCtx '::> x1) '::> t) '::> x3) '::> x4) '::> x5)
'::> x6)
'::> x7)
'::> x8)
u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
n)
where n :: MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
n = MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ)))))
-> MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
-> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR
instance Lens.Field3 (Assignment8 f x1 x2 t x4 x5 x6 x7 x8)
(Assignment8 f x1 x2 u x4 x5 x6 x7 x8)
(f t)
(f u) where
_3 :: Lens
(Assignment8 f x1 x2 t x4 x5 x6 x7 x8)
(Assignment8 f x1 x2 u x4 x5 x6 x7 x8)
(f t)
(f u)
_3 = (Assignment8 f x1 x2 t x4 x5 x6 x7 x8 -> f t)
-> (Assignment8 f x1 x2 t x4 x5 x6 x7 x8
-> f u -> Assignment8 f x1 x2 u x4 x5 x6 x7 x8)
-> Lens
(Assignment8 f x1 x2 t x4 x5 x6 x7 x8)
(Assignment8 f x1 x2 u x4 x5 x6 x7 x8)
(f t)
(f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
-> Assignment8 f x1 x2 t x4 x5 x6 x7 x8
-> MyNatLookup
(MyS (MyS (MyS (MyS (MyS 'MyZ)))))
(((((((('EmptyCtx '::> x1) '::> x2) '::> t) '::> x4) '::> x5)
'::> x6)
'::> x7)
'::> x8)
f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
n) (MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
-> Assignment8 f x1 x2 t x4 x5 x6 x7 x8
-> f u
-> Assignment
f
(StrongCtxUpdate
(MyS (MyS (MyS (MyS (MyS 'MyZ)))))
(((((((('EmptyCtx '::> x1) '::> x2) '::> t) '::> x4) '::> x5)
'::> x6)
'::> x7)
'::> x8)
u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
n)
where n :: MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
n = MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ)))))
-> MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
-> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR
instance Lens.Field4 (Assignment8 f x1 x2 x3 t x5 x6 x7 x8)
(Assignment8 f x1 x2 x3 u x5 x6 x7 x8)
(f t)
(f u) where
_4 :: Lens
(Assignment8 f x1 x2 x3 t x5 x6 x7 x8)
(Assignment8 f x1 x2 x3 u x5 x6 x7 x8)
(f t)
(f u)
_4 = (Assignment8 f x1 x2 x3 t x5 x6 x7 x8 -> f t)
-> (Assignment8 f x1 x2 x3 t x5 x6 x7 x8
-> f u -> Assignment8 f x1 x2 x3 u x5 x6 x7 x8)
-> Lens
(Assignment8 f x1 x2 x3 t x5 x6 x7 x8)
(Assignment8 f x1 x2 x3 u x5 x6 x7 x8)
(f t)
(f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> Assignment8 f x1 x2 x3 t x5 x6 x7 x8
-> MyNatLookup
(MyS (MyS (MyS (MyS 'MyZ))))
(((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> t) '::> x5)
'::> x6)
'::> x7)
'::> x8)
f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
n) (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> Assignment8 f x1 x2 x3 t x5 x6 x7 x8
-> f u
-> Assignment
f
(StrongCtxUpdate
(MyS (MyS (MyS (MyS 'MyZ))))
(((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> t) '::> x5)
'::> x6)
'::> x7)
'::> x8)
u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
n)
where n :: MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
n = MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ)))))
-> MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
-> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR
instance Lens.Field5 (Assignment8 f x1 x2 x3 x4 t x6 x7 x8)
(Assignment8 f x1 x2 x3 x4 u x6 x7 x8)
(f t)
(f u) where
_5 :: Lens
(Assignment8 f x1 x2 x3 x4 t x6 x7 x8)
(Assignment8 f x1 x2 x3 x4 u x6 x7 x8)
(f t)
(f u)
_5 = (Assignment8 f x1 x2 x3 x4 t x6 x7 x8 -> f t)
-> (Assignment8 f x1 x2 x3 x4 t x6 x7 x8
-> f u -> Assignment8 f x1 x2 x3 x4 u x6 x7 x8)
-> Lens
(Assignment8 f x1 x2 x3 x4 t x6 x7 x8)
(Assignment8 f x1 x2 x3 x4 u x6 x7 x8)
(f t)
(f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> Assignment8 f x1 x2 x3 x4 t x6 x7 x8
-> MyNatLookup
(MyS (MyS (MyS 'MyZ)))
(((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> t)
'::> x6)
'::> x7)
'::> x8)
f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS 'MyZ)))
n) (MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> Assignment8 f x1 x2 x3 x4 t x6 x7 x8
-> f u
-> Assignment
f
(StrongCtxUpdate
(MyS (MyS (MyS 'MyZ)))
(((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> t)
'::> x6)
'::> x7)
'::> x8)
u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS 'MyZ)))
n)
where n :: MyNatRepr (MyS (MyS (MyS 'MyZ)))
n = MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
-> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR
instance Lens.Field6 (Assignment8 f x1 x2 x3 x4 x5 t x7 x8)
(Assignment8 f x1 x2 x3 x4 x5 u x7 x8)
(f t)
(f u) where
_6 :: Lens
(Assignment8 f x1 x2 x3 x4 x5 t x7 x8)
(Assignment8 f x1 x2 x3 x4 x5 u x7 x8)
(f t)
(f u)
_6 = (Assignment8 f x1 x2 x3 x4 x5 t x7 x8 -> f t)
-> (Assignment8 f x1 x2 x3 x4 x5 t x7 x8
-> f u -> Assignment8 f x1 x2 x3 x4 x5 u x7 x8)
-> Lens
(Assignment8 f x1 x2 x3 x4 x5 t x7 x8)
(Assignment8 f x1 x2 x3 x4 x5 u x7 x8)
(f t)
(f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr (MyS (MyS 'MyZ))
-> Assignment8 f x1 x2 x3 x4 x5 t x7 x8
-> MyNatLookup
(MyS (MyS 'MyZ))
(((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
'::> t)
'::> x7)
'::> x8)
f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS 'MyZ))
n) (MyNatRepr (MyS (MyS 'MyZ))
-> Assignment8 f x1 x2 x3 x4 x5 t x7 x8
-> f u
-> Assignment
f
(StrongCtxUpdate
(MyS (MyS 'MyZ))
(((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
'::> t)
'::> x7)
'::> x8)
u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS 'MyZ))
n)
where n :: MyNatRepr (MyS (MyS 'MyZ))
n = MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
-> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR
instance Lens.Field7 (Assignment8 f x1 x2 x3 x4 x5 x6 t x8)
(Assignment8 f x1 x2 x3 x4 x5 x6 u x8)
(f t)
(f u) where
_7 :: Lens
(Assignment8 f x1 x2 x3 x4 x5 x6 t x8)
(Assignment8 f x1 x2 x3 x4 x5 x6 u x8)
(f t)
(f u)
_7 = (Assignment8 f x1 x2 x3 x4 x5 x6 t x8 -> f t)
-> (Assignment8 f x1 x2 x3 x4 x5 x6 t x8
-> f u -> Assignment8 f x1 x2 x3 x4 x5 x6 u x8)
-> Lens
(Assignment8 f x1 x2 x3 x4 x5 x6 t x8)
(Assignment8 f x1 x2 x3 x4 x5 x6 u x8)
(f t)
(f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr (MyS 'MyZ)
-> Assignment8 f x1 x2 x3 x4 x5 x6 t x8
-> MyNatLookup
(MyS 'MyZ)
(((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
'::> x6)
'::> t)
'::> x8)
f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS 'MyZ)
n) (MyNatRepr (MyS 'MyZ)
-> Assignment8 f x1 x2 x3 x4 x5 x6 t x8
-> f u
-> Assignment
f
(StrongCtxUpdate
(MyS 'MyZ)
(((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
'::> x6)
'::> t)
'::> x8)
u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS 'MyZ)
n)
where n :: MyNatRepr (MyS 'MyZ)
n = MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
-> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR
instance Lens.Field8 (Assignment8 f x1 x2 x3 x4 x5 x6 x7 t)
(Assignment8 f x1 x2 x3 x4 x5 x6 x7 u)
(f t)
(f u) where
_8 :: Lens
(Assignment8 f x1 x2 x3 x4 x5 x6 x7 t)
(Assignment8 f x1 x2 x3 x4 x5 x6 x7 u)
(f t)
(f u)
_8 = (Assignment8 f x1 x2 x3 x4 x5 x6 x7 t -> f t)
-> (Assignment8 f x1 x2 x3 x4 x5 x6 x7 t
-> f u -> Assignment8 f x1 x2 x3 x4 x5 x6 x7 u)
-> Lens
(Assignment8 f x1 x2 x3 x4 x5 x6 x7 t)
(Assignment8 f x1 x2 x3 x4 x5 x6 x7 u)
(f t)
(f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr 'MyZ
-> Assignment8 f x1 x2 x3 x4 x5 x6 x7 t
-> MyNatLookup
'MyZ
(((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
'::> x6)
'::> x7)
'::> t)
f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr 'MyZ
n) (MyNatRepr 'MyZ
-> Assignment8 f x1 x2 x3 x4 x5 x6 x7 t
-> f u
-> Assignment
f
(StrongCtxUpdate
'MyZ
(((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
'::> x6)
'::> x7)
'::> t)
u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr 'MyZ
n)
where n :: MyNatRepr 'MyZ
n = MyNatRepr 'MyZ
MyZR
type Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 x9
= Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4 '::> x5 '::> x6 '::> x7 '::> x8 '::> x9)
instance Lens.Field1 (Assignment9 f t x2 x3 x4 x5 x6 x7 x8 x9)
(Assignment9 f u x2 x3 x4 x5 x6 x7 x8 x9)
(f t)
(f u) where
_1 :: Lens
(Assignment9 f t x2 x3 x4 x5 x6 x7 x8 x9)
(Assignment9 f u x2 x3 x4 x5 x6 x7 x8 x9)
(f t)
(f u)
_1 = (Assignment9 f t x2 x3 x4 x5 x6 x7 x8 x9 -> f t)
-> (Assignment9 f t x2 x3 x4 x5 x6 x7 x8 x9
-> f u -> Assignment9 f u x2 x3 x4 x5 x6 x7 x8 x9)
-> Lens
(Assignment9 f t x2 x3 x4 x5 x6 x7 x8 x9)
(Assignment9 f u x2 x3 x4 x5 x6 x7 x8 x9)
(f t)
(f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))))
-> Assignment9 f t x2 x3 x4 x5 x6 x7 x8 x9
-> MyNatLookup
(MyS (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))))
((((((((('EmptyCtx '::> t) '::> x2) '::> x3) '::> x4) '::> x5)
'::> x6)
'::> x7)
'::> x8)
'::> x9)
f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))))
n) (MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))))
-> Assignment9 f t x2 x3 x4 x5 x6 x7 x8 x9
-> f u
-> Assignment
f
(StrongCtxUpdate
(MyS (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))))
((((((((('EmptyCtx '::> t) '::> x2) '::> x3) '::> x4) '::> x5)
'::> x6)
'::> x7)
'::> x8)
'::> x9)
u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))))
n)
where n :: MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))))
n = MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ)))))
-> MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
-> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR
instance Lens.Field2 (Assignment9 f x1 t x3 x4 x5 x6 x7 x8 x9)
(Assignment9 f x1 u x3 x4 x5 x6 x7 x8 x9)
(f t)
(f u) where
_2 :: Lens
(Assignment9 f x1 t x3 x4 x5 x6 x7 x8 x9)
(Assignment9 f x1 u x3 x4 x5 x6 x7 x8 x9)
(f t)
(f u)
_2 = (Assignment9 f x1 t x3 x4 x5 x6 x7 x8 x9 -> f t)
-> (Assignment9 f x1 t x3 x4 x5 x6 x7 x8 x9
-> f u -> Assignment9 f x1 u x3 x4 x5 x6 x7 x8 x9)
-> Lens
(Assignment9 f x1 t x3 x4 x5 x6 x7 x8 x9)
(Assignment9 f x1 u x3 x4 x5 x6 x7 x8 x9)
(f t)
(f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
-> Assignment9 f x1 t x3 x4 x5 x6 x7 x8 x9
-> MyNatLookup
(MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
((((((((('EmptyCtx '::> x1) '::> t) '::> x3) '::> x4) '::> x5)
'::> x6)
'::> x7)
'::> x8)
'::> x9)
f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
n) (MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
-> Assignment9 f x1 t x3 x4 x5 x6 x7 x8 x9
-> f u
-> Assignment
f
(StrongCtxUpdate
(MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
((((((((('EmptyCtx '::> x1) '::> t) '::> x3) '::> x4) '::> x5)
'::> x6)
'::> x7)
'::> x8)
'::> x9)
u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
n)
where n :: MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
n = MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ)))))
-> MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
-> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR
instance Lens.Field3 (Assignment9 f x1 x2 t x4 x5 x6 x7 x8 x9)
(Assignment9 f x1 x2 u x4 x5 x6 x7 x8 x9)
(f t)
(f u) where
_3 :: Lens
(Assignment9 f x1 x2 t x4 x5 x6 x7 x8 x9)
(Assignment9 f x1 x2 u x4 x5 x6 x7 x8 x9)
(f t)
(f u)
_3 = (Assignment9 f x1 x2 t x4 x5 x6 x7 x8 x9 -> f t)
-> (Assignment9 f x1 x2 t x4 x5 x6 x7 x8 x9
-> f u -> Assignment9 f x1 x2 u x4 x5 x6 x7 x8 x9)
-> Lens
(Assignment9 f x1 x2 t x4 x5 x6 x7 x8 x9)
(Assignment9 f x1 x2 u x4 x5 x6 x7 x8 x9)
(f t)
(f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
-> Assignment9 f x1 x2 t x4 x5 x6 x7 x8 x9
-> MyNatLookup
(MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
((((((((('EmptyCtx '::> x1) '::> x2) '::> t) '::> x4) '::> x5)
'::> x6)
'::> x7)
'::> x8)
'::> x9)
f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
n) (MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
-> Assignment9 f x1 x2 t x4 x5 x6 x7 x8 x9
-> f u
-> Assignment
f
(StrongCtxUpdate
(MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
((((((((('EmptyCtx '::> x1) '::> x2) '::> t) '::> x4) '::> x5)
'::> x6)
'::> x7)
'::> x8)
'::> x9)
u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
n)
where n :: MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
n = MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ)))))
-> MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
-> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR
instance Lens.Field4 (Assignment9 f x1 x2 x3 t x5 x6 x7 x8 x9)
(Assignment9 f x1 x2 x3 u x5 x6 x7 x8 x9)
(f t)
(f u) where
_4 :: Lens
(Assignment9 f x1 x2 x3 t x5 x6 x7 x8 x9)
(Assignment9 f x1 x2 x3 u x5 x6 x7 x8 x9)
(f t)
(f u)
_4 = (Assignment9 f x1 x2 x3 t x5 x6 x7 x8 x9 -> f t)
-> (Assignment9 f x1 x2 x3 t x5 x6 x7 x8 x9
-> f u -> Assignment9 f x1 x2 x3 u x5 x6 x7 x8 x9)
-> Lens
(Assignment9 f x1 x2 x3 t x5 x6 x7 x8 x9)
(Assignment9 f x1 x2 x3 u x5 x6 x7 x8 x9)
(f t)
(f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
-> Assignment9 f x1 x2 x3 t x5 x6 x7 x8 x9
-> MyNatLookup
(MyS (MyS (MyS (MyS (MyS 'MyZ)))))
((((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> t) '::> x5)
'::> x6)
'::> x7)
'::> x8)
'::> x9)
f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
n) (MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
-> Assignment9 f x1 x2 x3 t x5 x6 x7 x8 x9
-> f u
-> Assignment
f
(StrongCtxUpdate
(MyS (MyS (MyS (MyS (MyS 'MyZ)))))
((((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> t) '::> x5)
'::> x6)
'::> x7)
'::> x8)
'::> x9)
u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
n)
where n :: MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
n = MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ)))))
-> MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
-> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR
instance Lens.Field5 (Assignment9 f x1 x2 x3 x4 t x6 x7 x8 x9)
(Assignment9 f x1 x2 x3 x4 u x6 x7 x8 x9)
(f t)
(f u) where
_5 :: Lens
(Assignment9 f x1 x2 x3 x4 t x6 x7 x8 x9)
(Assignment9 f x1 x2 x3 x4 u x6 x7 x8 x9)
(f t)
(f u)
_5 = (Assignment9 f x1 x2 x3 x4 t x6 x7 x8 x9 -> f t)
-> (Assignment9 f x1 x2 x3 x4 t x6 x7 x8 x9
-> f u -> Assignment9 f x1 x2 x3 x4 u x6 x7 x8 x9)
-> Lens
(Assignment9 f x1 x2 x3 x4 t x6 x7 x8 x9)
(Assignment9 f x1 x2 x3 x4 u x6 x7 x8 x9)
(f t)
(f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> Assignment9 f x1 x2 x3 x4 t x6 x7 x8 x9
-> MyNatLookup
(MyS (MyS (MyS (MyS 'MyZ))))
((((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> t)
'::> x6)
'::> x7)
'::> x8)
'::> x9)
f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
n) (MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
-> Assignment9 f x1 x2 x3 x4 t x6 x7 x8 x9
-> f u
-> Assignment
f
(StrongCtxUpdate
(MyS (MyS (MyS (MyS 'MyZ))))
((((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> t)
'::> x6)
'::> x7)
'::> x8)
'::> x9)
u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
n)
where n :: MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
n = MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ)))))
-> MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
-> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR
instance Lens.Field6 (Assignment9 f x1 x2 x3 x4 x5 t x7 x8 x9)
(Assignment9 f x1 x2 x3 x4 x5 u x7 x8 x9)
(f t)
(f u) where
_6 :: Lens
(Assignment9 f x1 x2 x3 x4 x5 t x7 x8 x9)
(Assignment9 f x1 x2 x3 x4 x5 u x7 x8 x9)
(f t)
(f u)
_6 = (Assignment9 f x1 x2 x3 x4 x5 t x7 x8 x9 -> f t)
-> (Assignment9 f x1 x2 x3 x4 x5 t x7 x8 x9
-> f u -> Assignment9 f x1 x2 x3 x4 x5 u x7 x8 x9)
-> Lens
(Assignment9 f x1 x2 x3 x4 x5 t x7 x8 x9)
(Assignment9 f x1 x2 x3 x4 x5 u x7 x8 x9)
(f t)
(f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> Assignment9 f x1 x2 x3 x4 x5 t x7 x8 x9
-> MyNatLookup
(MyS (MyS (MyS 'MyZ)))
((((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
'::> t)
'::> x7)
'::> x8)
'::> x9)
f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS 'MyZ)))
n) (MyNatRepr (MyS (MyS (MyS 'MyZ)))
-> Assignment9 f x1 x2 x3 x4 x5 t x7 x8 x9
-> f u
-> Assignment
f
(StrongCtxUpdate
(MyS (MyS (MyS 'MyZ)))
((((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
'::> t)
'::> x7)
'::> x8)
'::> x9)
u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS 'MyZ)))
n)
where n :: MyNatRepr (MyS (MyS (MyS 'MyZ)))
n = MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ))))
-> MyNatRepr (MyS (MyS 'MyZ)) -> MyNatRepr (MyS (MyS (MyS 'MyZ)))
forall a b. (a -> b) -> a -> b
$ MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
-> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR
instance Lens.Field7 (Assignment9 f x1 x2 x3 x4 x5 x6 t x8 x9)
(Assignment9 f x1 x2 x3 x4 x5 x6 u x8 x9)
(f t)
(f u) where
_7 :: Lens
(Assignment9 f x1 x2 x3 x4 x5 x6 t x8 x9)
(Assignment9 f x1 x2 x3 x4 x5 x6 u x8 x9)
(f t)
(f u)
_7 = (Assignment9 f x1 x2 x3 x4 x5 x6 t x8 x9 -> f t)
-> (Assignment9 f x1 x2 x3 x4 x5 x6 t x8 x9
-> f u -> Assignment9 f x1 x2 x3 x4 x5 x6 u x8 x9)
-> Lens
(Assignment9 f x1 x2 x3 x4 x5 x6 t x8 x9)
(Assignment9 f x1 x2 x3 x4 x5 x6 u x8 x9)
(f t)
(f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr (MyS (MyS 'MyZ))
-> Assignment9 f x1 x2 x3 x4 x5 x6 t x8 x9
-> MyNatLookup
(MyS (MyS 'MyZ))
((((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
'::> x6)
'::> t)
'::> x8)
'::> x9)
f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS 'MyZ))
n) (MyNatRepr (MyS (MyS 'MyZ))
-> Assignment9 f x1 x2 x3 x4 x5 x6 t x8 x9
-> f u
-> Assignment
f
(StrongCtxUpdate
(MyS (MyS 'MyZ))
((((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
'::> x6)
'::> t)
'::> x8)
'::> x9)
u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS 'MyZ))
n)
where n :: MyNatRepr (MyS (MyS 'MyZ))
n = MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ)))
-> MyNatRepr (MyS 'MyZ) -> MyNatRepr (MyS (MyS 'MyZ))
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
-> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR
instance Lens.Field8 (Assignment9 f x1 x2 x3 x4 x5 x6 x7 t x9)
(Assignment9 f x1 x2 x3 x4 x5 x6 x7 u x9)
(f t)
(f u) where
_8 :: Lens
(Assignment9 f x1 x2 x3 x4 x5 x6 x7 t x9)
(Assignment9 f x1 x2 x3 x4 x5 x6 x7 u x9)
(f t)
(f u)
_8 = (Assignment9 f x1 x2 x3 x4 x5 x6 x7 t x9 -> f t)
-> (Assignment9 f x1 x2 x3 x4 x5 x6 x7 t x9
-> f u -> Assignment9 f x1 x2 x3 x4 x5 x6 x7 u x9)
-> Lens
(Assignment9 f x1 x2 x3 x4 x5 x6 x7 t x9)
(Assignment9 f x1 x2 x3 x4 x5 x6 x7 u x9)
(f t)
(f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr (MyS 'MyZ)
-> Assignment9 f x1 x2 x3 x4 x5 x6 x7 t x9
-> MyNatLookup
(MyS 'MyZ)
((((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
'::> x6)
'::> x7)
'::> t)
'::> x9)
f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS 'MyZ)
n) (MyNatRepr (MyS 'MyZ)
-> Assignment9 f x1 x2 x3 x4 x5 x6 x7 t x9
-> f u
-> Assignment
f
(StrongCtxUpdate
(MyS 'MyZ)
((((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
'::> x6)
'::> x7)
'::> t)
'::> x9)
u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS 'MyZ)
n)
where n :: MyNatRepr (MyS 'MyZ)
n = MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR (MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ))
-> MyNatRepr 'MyZ -> MyNatRepr (MyS 'MyZ)
forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR
instance Lens.Field9 (Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 t)
(Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 u)
(f t)
(f u) where
_9 :: Lens
(Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 t)
(Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 u)
(f t)
(f u)
_9 = (Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 t -> f t)
-> (Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 t
-> f u -> Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 u)
-> Lens
(Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 t)
(Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 u)
(f t)
(f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (MyNatRepr 'MyZ
-> Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 t
-> MyNatLookup
'MyZ
((((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
'::> x6)
'::> x7)
'::> x8)
'::> t)
f
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr 'MyZ
n) (MyNatRepr 'MyZ
-> Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 t
-> f u
-> Assignment
f
(StrongCtxUpdate
'MyZ
((((((((('EmptyCtx '::> x1) '::> x2) '::> x3) '::> x4) '::> x5)
'::> x6)
'::> x7)
'::> x8)
'::> t)
u)
forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr 'MyZ
n)
where n :: MyNatRepr 'MyZ
n = MyNatRepr 'MyZ
MyZR