Fix totality of rebuildEnv
commit6c3d33c93a8894b1c57c21d55a4cb06e02953c20
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateFri 11 Apr 2014, 12:03 (13 years ago)
parent8cd3ea5
libs/effects/Effects.idr+2
@@ -96,6 +96,8 @@ rebuildEnv [] SubNil env = env
9696rebuildEnv (x :: xs) (Keep rest) (y :: env) = x :: rebuildEnv xs rest env
9797rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env
9898rebuildEnv (x :: xs) SubNil [] = x :: xs
99+rebuildEnv [] (Keep x) (x :: xs) = []
100+
99101
100102-- -------------------------------------------------- [ The Effect EDSL itself ]
101103-- some proof automation