diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2024-10-28 15:34:16 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2024-10-28 15:34:16 +0000 |
| commit | e258c78a5ab9529242b4c8fa168eda85430e641e (patch) | |
| tree | 939ced9a71c94736222d05616a46dfc7292accd0 /src/Inky/Data/Thinned.idr | |
| parent | d926ce9f2d1144f329598a30b3ed2e48899519b2 (diff) | |
Make everything relevant.
Too few proofs were relevant. Now they are.
Diffstat (limited to 'src/Inky/Data/Thinned.idr')
| -rw-r--r-- | src/Inky/Data/Thinned.idr | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/src/Inky/Data/Thinned.idr b/src/Inky/Data/Thinned.idr new file mode 100644 index 0000000..6ee0d50 --- /dev/null +++ b/src/Inky/Data/Thinned.idr @@ -0,0 +1,18 @@ +module Inky.Data.Thinned + +import public Inky.Data.SnocList.Thinning + +public export +record Thinned (0 p : SnocList a -> Type) (ctx : SnocList a) where + constructor Over + {0 support : SnocList a} + value : p support + thins : support `Thins` ctx + +public export +rename : (ctx1 `Thins` ctx2) -> Thinned p ctx1 -> Thinned p ctx2 +rename f (value `Over` thins) = value `Over` (f . thins) + +public export +(.extract) : Rename a p => Thinned p ctx -> p ctx +(value `Over` thins).extract = rename thins value |