diff options
Diffstat (limited to 'src/AST/Weaken.hs')
| -rw-r--r-- | src/AST/Weaken.hs | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/AST/Weaken.hs b/src/AST/Weaken.hs index 0a1e4ce..ecd7bc9 100644 --- a/src/AST/Weaken.hs +++ b/src/AST/Weaken.hs @@ -48,7 +48,7 @@ data env :> env' where -> Append pre (t : env) :> t : Append pre env' WSwap :: forall env as bs. SList (Const ()) as -> SList (Const ()) bs -> Append as (Append bs env) :> Append bs (Append as env) - WStack :: forall as bs env1 env2. SList (Const ()) as -> SList (Const ()) bs + WStack :: forall env1 env2 as bs. SList (Const ()) as -> SList (Const ()) bs -> as :> bs -> env1 :> env2 -> Append as env1 :> Append bs env2 deriving instance Show (env :> env') @@ -74,7 +74,7 @@ WSwap @env (as :: SList _ as) (bs :: SList _ bs) @> i = Right i' -> case splitIdx @env bs i' of Left j -> indexRaiseAbove @(Append as env) bs j Right j -> indexSinks bs (indexSinks as j) -WStack @as @bs @env1 @env2 as bs wlo whi @> i = +WStack @env1 @env2 as bs wlo whi @> i = case splitIdx @env1 as i of Left i' -> indexRaiseAbove @env2 bs (wlo @> i') Right i' -> indexSinks bs (whi @> i') |