git.iko.soy/Idris-dev
on master help sign in
Fix totality of rebuildEnv
6c3d33cEdwin Brady
libs/effects/Effects.idr+2
compare with master
unifiedsplit
@@ -96,6 +96,8 @@ rebuildEnv [] SubNil env = env
96rebuildEnv (x :: xs) (Keep rest) (y :: env) = x :: rebuildEnv xs rest env
96rebuildEnv (x :: xs) (Keep rest) (y :: env) = x :: rebuildEnv xs rest env
97rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env
97rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env
98rebuildEnv (x :: xs) SubNil [] = x :: xs
98rebuildEnv (x :: xs) SubNil [] = x :: xs
99+rebuildEnv [] (Keep x) (x :: xs) = []
100+
99
101
100-- -------------------------------------------------- [ The Effect EDSL itself ]
102-- -------------------------------------------------- [ The Effect EDSL itself ]
101-- some proof automation
103-- some proof automation