@@ -48,6 +48,8 @@ updateWith : (ys' : List a) -> (xs : List a) ->
4848updateWith (y :: ys) (x :: xs) (Keep rest) = y :: updateWith ys xs rest
4949updateWith ys (x :: xs) (Drop rest) = x :: updateWith ys xs rest
5050updateWith [] [] SubNil = []
51+updateWith (y :: ys) [] SubNil = y :: ys
52+updateWith [] (x :: xs) (Keep rest) = []
5153
5254-- put things back, replacing old with new in the sub-environment
5355rebuildEnv : Env m ys' -> (prf : SubList ys xs) ->
@@ -55,6 +57,7 @@ rebuildEnv : Env m ys' -> (prf : SubList ys xs) ->
5557rebuildEnv [] SubNil env = env
5658rebuildEnv (x :: xs) (Keep rest) (y :: env) = x :: rebuildEnv xs rest env
5759rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env
60+rebuildEnv (x :: xs) SubNil [] = x :: xs
5861
5962---- The Effect EDSL itself ----
6063
@@ -210,4 +213,3 @@ mapE f (x :: xs) = [| f x :: mapE f xs |]
210213when : Applicative m => Bool -> Eff m xs () -> Eff m xs ()
211214when True e = e
212215when False e = pure ()
213−