@@ -48,6 +48,8 @@ updateWith : (ys' : List a) -> (xs : List a) ->
48updateWith (y :: ys) (x :: xs) (Keep rest) = y :: updateWith ys xs rest
48updateWith (y :: ys) (x :: xs) (Keep rest) = y :: updateWith ys xs rest
49updateWith ys (x :: xs) (Drop rest) = x :: updateWith ys xs rest
49updateWith ys (x :: xs) (Drop rest) = x :: updateWith ys xs rest
50updateWith [] [] SubNil = []
50updateWith [] [] SubNil = []
51+updateWith (y :: ys) [] SubNil = y :: ys
52+updateWith [] (x :: xs) (Keep rest) = []
52-- put things back, replacing old with new in the sub-environment
54-- put things back, replacing old with new in the sub-environment
53rebuildEnv : Env m ys' -> (prf : SubList ys xs) ->
55rebuildEnv : Env m ys' -> (prf : SubList ys xs) ->
@@ -55,6 +57,7 @@ rebuildEnv : Env m ys' -> (prf : SubList ys xs) ->
55rebuildEnv [] SubNil env = env
57rebuildEnv [] SubNil env = env
56rebuildEnv (x :: xs) (Keep rest) (y :: env) = x :: rebuildEnv xs rest env
58rebuildEnv (x :: xs) (Keep rest) (y :: env) = x :: rebuildEnv xs rest env
57rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env
59rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env
60+rebuildEnv (x :: xs) SubNil [] = x :: xs
59---- The Effect EDSL itself ----
62---- The Effect EDSL itself ----
@@ -210,4 +213,3 @@ mapE f (x :: xs) = [| f x :: mapE f xs |]
210when : Applicative m => Bool -> Eff m xs () -> Eff m xs ()
213when : Applicative m => Bool -> Eff m xs () -> Eff m xs ()
211when True e = e
214when True e = e
212when False e = pure ()
215when False e = pure ()