diff options
Diffstat (limited to 'src/Inky/Data/SnocList/Thinning.idr')
| -rw-r--r-- | src/Inky/Data/SnocList/Thinning.idr | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/Inky/Data/SnocList/Thinning.idr b/src/Inky/Data/SnocList/Thinning.idr index f766069..60666d2 100644 --- a/src/Inky/Data/SnocList/Thinning.idr +++ b/src/Inky/Data/SnocList/Thinning.idr @@ -2,6 +2,7 @@ module Inky.Data.SnocList.Thinning import Data.DPair import Data.Nat +import Inky.Data.List import Inky.Data.SnocList import Inky.Data.SnocList.Var import Inky.Data.SnocList.Quantifiers @@ -97,6 +98,16 @@ prf.index ((%%) n {pos}) = irrelevantEq $ toVarCong $ toNatInjective $ prf.index -- Useful for Parsers ---------------------------------------------------------- public export +(<><) : ctx1 `Thins` ctx2 -> LengthOf bound -> ctx1 <>< bound `Thins` ctx2 <>< bound +f <>< Z = f +f <>< S len = Keep f <>< len + +public export +dropFish : ctx1 `Thins` ctx2 -> LengthOf bound -> ctx1 `Thins` ctx2 <>< bound +dropFish f Z = f +dropFish f (S len) = dropFish (Drop f) len + +public export dropPos : (pos : Elem x ctx) -> dropElem ctx pos `Thins` ctx dropPos Here = Drop Id dropPos (There pos) = Keep (dropPos pos) |