diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-06 16:57:25 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-06 16:57:25 +0100 |
| commit | 93aae7e34e7130d9541d3441079448f156d93477 (patch) | |
| tree | 02900fd5e8588e7d04e5375488b70bb12aa4a788 /src/Core/Term.idr | |
| parent | fce659187d9e24e29ae23f7d8de078dcdc9dcfd4 (diff) | |
Migrate Env to use Thinned.
Diffstat (limited to 'src/Core/Term.idr')
| -rw-r--r-- | src/Core/Term.idr | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/Core/Term.idr b/src/Core/Term.idr index e52545d..182e1ea 100644 --- a/src/Core/Term.idr +++ b/src/Core/Term.idr @@ -81,3 +81,11 @@ expandShift : (thin : sx `Thins` sy) -> expand (shift t thin) = wkn (expand t) thin expandShift (term `Over` thin') thin = sym $ wknHomo term thin' thin + +export +shiftHomo : + (t : Thinned sx) -> + (thin1 : sx `Thins` sy) -> + (thin2 : sy `Thins` sz) -> + shift (shift t thin1) thin2 = shift t (thin2 . thin1) +shiftHomo (term `Over` thin) thin1 thin2 = cong (term `Over`) $ compAssoc thin2 thin1 thin |