From 69b82b0f568dd840f05f6aa9902ee6dcd5df5cad Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Tue, 8 Mar 2022 18:49:39 +0000 Subject: Migrate to agda-stdlib-2.0-dev. --- src/Helium/Semantics/Axiomatic/Term.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/Helium/Semantics/Axiomatic/Term.agda') diff --git a/src/Helium/Semantics/Axiomatic/Term.agda b/src/Helium/Semantics/Axiomatic/Term.agda index c7c2797..e9a3f4a 100644 --- a/src/Helium/Semantics/Axiomatic/Term.agda +++ b/src/Helium/Semantics/Axiomatic/Term.agda @@ -102,7 +102,7 @@ wknVar (func f ts) = func f (helper ts) wknVars : (ts : Vec Type n) → Term Σ Γ Δ t → Term Σ (ts ++ Γ) Δ t wknVars τs (state i) = state i -wknVars τs (var i) = castType (var (Fin.raise (Vec.length τs) i)) (Vecₚ.lookup-++ʳ τs _ i) +wknVars τs (var i) = castType (var (Vec.length τs Fin.↑ʳ i)) (Vecₚ.lookup-++ʳ τs _ i) wknVars τs (meta i) = meta i wknVars τs (func f ts) = func f (helper ts) where @@ -135,7 +135,7 @@ wknMeta = wknMetaAt 0F wknMetas : (ts : Vec Type n) → Term Σ Γ Δ t → Term Σ Γ (ts ++ Δ) t wknMetas τs (state i) = state i wknMetas τs (var i) = var i -wknMetas τs (meta i) = castType (meta (Fin.raise (Vec.length τs) i)) (Vecₚ.lookup-++ʳ τs _ i) +wknMetas τs (meta i) = castType (meta (Vec.length τs Fin.↑ʳ i)) (Vecₚ.lookup-++ʳ τs _ i) wknMetas τs (func f ts) = func f (helper ts) where helper : ∀ {n ts} → All (Term Σ Γ Δ) {n} ts → All (Term Σ Γ (τs ++ Δ)) ts -- cgit v1.2.3