From 87eea439d8d8390c768498c2224268200373f629 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Sun, 16 Apr 2023 18:31:20 +0100 Subject: Prove weakening of type judgements. This is a huge commit that has many more changes. I should split this up later. --- src/Core/Environment.idr | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'src/Core/Environment.idr') 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 _) -- cgit v1.2.3