diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2024-11-12 16:44:31 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2024-11-12 16:44:31 +0000 |
| commit | ecaf9deb4b1d2ce85617438e621690b2df3ea367 (patch) | |
| tree | f7f347a847ca58668349ee44e1bf047bff385600 /src/Inky/Data/SnocList/Elem.idr | |
| parent | 66169116cbacff64950407086fd0d832516a5f21 (diff) | |
Add ability to desugar terms.
Remove `getChildren` construct---it's too niche for the core language.
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 |