diff options
Diffstat (limited to 'src/Inky/Data/SnocList/Elem.idr')
| -rw-r--r-- | src/Inky/Data/SnocList/Elem.idr | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/Inky/Data/SnocList/Elem.idr b/src/Inky/Data/SnocList/Elem.idr index 465e92c..c1e69f6 100644 --- a/src/Inky/Data/SnocList/Elem.idr +++ b/src/Inky/Data/SnocList/Elem.idr @@ -8,6 +8,7 @@ import Data.Singleton import Inky.Decidable import Inky.Decidable.Maybe import Inky.Data.Assoc +import Inky.Data.List import Inky.Data.SnocList export @@ -71,6 +72,11 @@ split Z pos = Left pos split (S len) Here = Right Here split (S len) (There pos) = mapSnd There $ split len pos +public export +wknL' : Elem x sx -> LengthOf xs -> Elem x (sx <>< xs) +wknL' i Z = i +wknL' i (S len) = wknL' (There i) len + -- Lookup ---------------------------------------------------------------------- export |