diff options
Diffstat (limited to 'src/Thinning.idr')
| -rw-r--r-- | src/Thinning.idr | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/Thinning.idr b/src/Thinning.idr index a79f0f5..a9b724d 100644 --- a/src/Thinning.idr +++ b/src/Thinning.idr @@ -31,6 +31,11 @@ keep Id = Id keep (Drop thin) = Keep (Drop thin) keep (Keep thin) = Keep (Keep thin) +public export +empty : (sx : SnocList a) -> [<] `Thins` sx +empty [<] = Id +empty (sx :< x) = Drop (empty sx) + -- Operations ------------------------------------------------------------------ public export |