diff options
Diffstat (limited to 'src/Core')
| -rw-r--r-- | src/Core/Term.idr | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/src/Core/Term.idr b/src/Core/Term.idr index 28e229d..e52545d 100644 --- a/src/Core/Term.idr +++ b/src/Core/Term.idr @@ -6,6 +6,8 @@ import Core.Thinning import Syntax.PreorderReasoning +%prefix_record_projections off + -- Definition ------------------------------------------------------------------ public export @@ -53,3 +55,29 @@ wknHomo (Abs n t) thin1 thin2 = ~~ wkn t (keep thin2 n . keep thin1 n) ...(wknHomo t (keep thin1 n) (keep thin2 n)) ~~ wkn t (keep (thin2 . thin1) n) ...(cong (wkn t) $ compKeep thin2 thin1 n) wknHomo (App t u) thin1 thin2 = cong2 App (wknHomo t thin1 thin2) (wknHomo u thin1 thin2) + +-- Thinned Terms --------------------------------------------------------------- + +public export +record Thinned (sx : Context) where + constructor Over + {0 sy : Context} + term : Term sy + thin : sy `Thins` sx + +%name Thinned t, u, v + +public export +expand : Thinned sx -> Term sx +expand (term `Over` thin) = wkn term thin + +public export +shift : Thinned sx -> sx `Thins` sy -> Thinned sy +shift (term `Over` thin') thin = term `Over` thin . thin' + +export +expandShift : + (t : Thinned sx) -> + (thin : sx `Thins` sy) -> + expand (shift t thin) = wkn (expand t) thin +expandShift (term `Over` thin') thin = sym $ wknHomo term thin' thin |