diff options
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 _) |