diff options
Diffstat (limited to 'src/Core/Thinning.idr')
| -rw-r--r-- | src/Core/Thinning.idr | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/src/Core/Thinning.idr b/src/Core/Thinning.idr index a41536e..f54d9e9 100644 --- a/src/Core/Thinning.idr +++ b/src/Core/Thinning.idr @@ -43,6 +43,21 @@ public export wkn1 : (0 sx : Context) -> (0 n : Name) -> sx `Thins` sx :< n wkn1 sx n = drop (id sx) n +-- Properties + +export +dropIsNotId : (thin : sx `Thins` sy) -> (0 n : Name) -> IsNotId (drop thin n) +dropIsNotId IsId n = ItIsThinner +dropIsNotId (IsThinner thinner) n = ItIsThinner + +export +keepIdIsId : (0 sx : Context) -> (0 n : Name) -> keep (id sx) n = id (sx :< n) +keepIdIsId sx n = Refl + +export +keepNotIdIsNotId : IsNotId thin -> (0 n : Name) -> IsNotId (keep thin n) +keepNotIdIsNotId ItIsThinner n = ItIsThinner + -- Views ----------------------------------------------------------------------- public export |