@@ -85,10 +85,12 @@ syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)
8585
8686-- --------------------------------------- [ Properties and Proof Construction ]
8787
88+public export
8889data SubElem : a -> List a -> Type where
8990 Z : SubElem a (a :: as)
9091 S : SubElem a as -> SubElem a (b :: as)
9192
93+public export
9294data SubList : List a -> List a -> Type where
9395 SubNil : SubList [] xs
9496 InList : SubElem x ys -> SubList xs ys -> SubList (x :: xs) ys
@@ -100,6 +102,7 @@ namespace Env
100102 (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
101103
102104namespace EffElem
105+ public export
103106 data EffElem : Effect -> Type ->
104107 List EFFECT -> Type where
105108 Here : EffElem x a (MkEff a x :: xs)
@@ -118,18 +121,21 @@ dropEnv e@(y::ys) (InList idx rest) =
118121 let [x] = envElem idx e
119122 in x :: dropEnv e rest
120123
124+public export
121125total updateAt : (idx : SubElem x' xs) -> (a:Type) -> List EFFECT -> List EFFECT
122126updateAt Z a [] = []
123127updateAt Z a ((MkEff b eff) :: xs) = (MkEff a eff) :: xs
124128updateAt (S k) a [] = []
125129updateAt (S k) a (x :: xs) = x :: updateAt k a xs
126130
131+public export
127132total updateWith : (ys' : List EFFECT) -> (xs : List EFFECT) ->
128133 SubList ys xs -> List EFFECT
129134updateWith [] xs sl = xs
130135updateWith (y :: ys) xs SubNil = xs
131136updateWith ((MkEff a f) :: ys) xs (InList idx rest) = updateAt idx a (updateWith ys xs rest)
132137
138+public export
133139total replaceEnvAt : (x : a) -> (idx : SubElem x' xs) -> Env m ys ->
134140 Env m (updateAt idx a ys)
135141replaceEnvAt x Z [] = []
@@ -138,6 +144,7 @@ replaceEnvAt x (S k) [] = []
138144replaceEnvAt x (S k) (y :: ys) = y :: replaceEnvAt x k ys
139145
140146||| Put things back, replacing old with new in the sub-environment
147+public export
141148total rebuildEnv : {ys':List EFFECT} -> Env m ys' -> (prf : SubList ys xs) ->
142149 Env m xs -> Env m (updateWith ys' xs prf)
143150rebuildEnv [] SubNil env = env