diff options
Diffstat (limited to 'src/AST/Weaken.hs')
| -rw-r--r-- | src/AST/Weaken.hs | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/AST/Weaken.hs b/src/AST/Weaken.hs index ecd7bc9..dbb37f7 100644 --- a/src/AST/Weaken.hs +++ b/src/AST/Weaken.hs @@ -42,7 +42,7 @@ data env :> env' where WCopy :: forall t env env'. env :> env' -> (t : env) :> (t : env') WPop :: (t : env) :> env' -> env :> env' WThen :: env1 :> env2 -> env2 :> env3 -> env1 :> env3 - WClosed :: SList (Const ()) env -> '[] :> env + WClosed :: '[] :> env WIdx :: Idx env t -> (t : env) :> env WPick :: forall t pre env env'. SList (Const ()) pre -> env :> env' -> Append pre (t : env) :> t : Append pre env' @@ -62,7 +62,7 @@ WCopy _ @> IZ = IZ WCopy w @> IS i = IS (w @> i) WPop w @> i = w @> IS i WThen w1 w2 @> i = w2 @> w1 @> i -WClosed _ @> i = case i of {} +WClosed @> i = case i of {} WIdx j @> IZ = j WIdx _ @> IS i = i WPick SNil w @> i = WCopy w @> i @@ -115,5 +115,5 @@ wCopies bs w = in WStack bs' bs' WId w wRaiseAbove :: SList f env1 -> SList g env -> env1 :> Append env1 env -wRaiseAbove SNil env = WClosed (slistMap (\_ -> Const ()) env) +wRaiseAbove SNil _ = WClosed wRaiseAbove (SCons _ s) env = WCopy (wRaiseAbove s env) |