diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2024-11-15 15:44:30 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2024-11-15 15:44:30 +0000 |
| commit | 3caa95a139538bb07c74847ca3aba2603a03c502 (patch) | |
| tree | afa588ecffb2efd05b1202c7ce5ae6005c86b8d2 /src/Inky/Data/Thinned.idr | |
| parent | 865dc549baf613e45e2f79036d54850a483fa509 (diff) | |
Add compilation to scheme.
Extract parser as an independent project.
Diffstat (limited to 'src/Inky/Data/Thinned.idr')
| -rw-r--r-- | src/Inky/Data/Thinned.idr | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/src/Inky/Data/Thinned.idr b/src/Inky/Data/Thinned.idr index 6ee0d50..eaf5e7b 100644 --- a/src/Inky/Data/Thinned.idr +++ b/src/Inky/Data/Thinned.idr @@ -1,6 +1,6 @@ module Inky.Data.Thinned -import public Inky.Data.SnocList.Thinning +import public Flap.Data.SnocList.Thinning public export record Thinned (0 p : SnocList a -> Type) (ctx : SnocList a) where @@ -11,8 +11,15 @@ record Thinned (0 p : SnocList a -> Type) (ctx : SnocList a) where public export rename : (ctx1 `Thins` ctx2) -> Thinned p ctx1 -> Thinned p ctx2 -rename f (value `Over` thins) = value `Over` (f . thins) +rename f v = v.value `Over` (f . v.thins) public export (.extract) : Rename a p => Thinned p ctx -> p ctx -(value `Over` thins).extract = rename thins value +v.extract = rename v.thins v.value + +export +0 extractHomo : + Rename a p => + (f : ctx1 `Thins` ctx2) -> (x : Thinned p ctx1) -> + rename f x.extract = (rename f x).extract +extractHomo f x = renameHomo f x.thins x.value |