diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-16 18:31:20 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-16 18:31:20 +0100 |
| commit | 87eea439d8d8390c768498c2224268200373f629 (patch) | |
| tree | ee0791e980d9f4679cb159f236be6e3228d0b46c /src/Core/Environment.idr | |
| parent | 4dbdc01e4819fcd5124ad108c4b00c10652bd3cc (diff) | |
Prove weakening of type judgements.
This is a huge commit that has many more changes. I should split
this up later.
Diffstat (limited to 'src/Core/Environment.idr')
| -rw-r--r-- | src/Core/Environment.idr | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/Core/Environment.idr b/src/Core/Environment.idr index f13cde3..cdf58b7 100644 --- a/src/Core/Environment.idr +++ b/src/Core/Environment.idr @@ -26,8 +26,8 @@ namespace Eq public export index : Env n -> Fin n -> Thinned n -index (env :< t) FZ = wkn t (drop $ id _) -index (env :< t) (FS i) = wkn (index env i) (drop $ id _) +index (env :< t) FZ = wkn t (wkn1 _) +index (env :< t) (FS i) = wkn (index env i) (wkn1 _) export indexCong : @@ -36,5 +36,5 @@ indexCong : (i : Fin n) -> index env1 i =~= index env2 i indexCong Refl i = Refl -indexCong (prf :< prf') FZ = wknCong prf' (drop $ id _) -indexCong (prf :< prf') (FS i) = wknCong (indexCong prf i) (drop $ id _) +indexCong (prf :< prf') FZ = wknCong prf' (wkn1 _) +indexCong (prf :< prf') (FS i) = wknCong (indexCong prf i) (wkn1 _) |