diff options
Diffstat (limited to 'src/Thinning.idr')
| -rw-r--r-- | src/Thinning.idr | 22 |
1 files changed, 7 insertions, 15 deletions
diff --git a/src/Thinning.idr b/src/Thinning.idr index f9e76b5..70165d0 100644 --- a/src/Thinning.idr +++ b/src/Thinning.idr @@ -26,24 +26,16 @@ data Len : SnocList a -> Type where %name Len k, m, n %hint -export +public export length : (sx : SnocList a) -> Len sx length [<] = Z length (sx :< x) = S (length sx) %hint export -lenSrc : sx `Thins` sy -> Len sx -lenSrc Empty = Z -lenSrc (Drop thin) = lenSrc thin -lenSrc (Keep thin) = S (lenSrc thin) - -%hint -export -lenTgt : sx `Thins` sy -> Len sy -lenTgt Empty = Z -lenTgt (Drop thin) = S (lenTgt thin) -lenTgt (Keep thin) = S (lenTgt thin) +lenAppend : Len sx -> Len sy -> Len (sx ++ sy) +lenAppend k Z = k +lenAppend k (S m) = S (lenAppend k m) %hint export @@ -101,6 +93,7 @@ data Triangle : sy `Thins` sz -> sx `Thins` sy -> sx `Thins` sz -> Type where KeepDrop : Triangle thin2 thin1 thin -> Triangle (Keep thin2) (Drop thin1) (Drop thin) KeepKeep : Triangle thin2 thin1 thin -> Triangle (Keep thin2) (Keep thin1) (Keep thin) +public export data Overlap = Covers | Partitions namespace Covering @@ -190,10 +183,9 @@ export map : (forall ctx. t ctx -> u ctx) -> Thinned t ctx -> Thinned u ctx map f (value `Over` thin) = f value `Over` thin -%hint export -thinnedLen : Thinned t sx -> Len sx -thinnedLen (value `Over` thin) = lenTgt thin +drop : Thinned t ctx -> Thinned t (ctx :< ty) +drop (value `Over` thin) = value `Over` Drop thin -- Properties ------------------------------------------------------------------ |