rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

loosen pushCoe's type slightly

Browse source
This commit is contained in:
rhiannon morris 2023-08-28 20:03:06 +02:00
parent add2eb400c
commit d5d30ee198
1 changed files with 3 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
lib/Quox/Whnf/Coercion.idr
View file

@ -97,8 +97,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
boxCoe qty sty@(S [< i] ty) p q val ret body loc = do boxCoe qty sty@(S [< i] ty) p q val ret body loc = do
-- caseπ (coe [i ⇒ [ρ. A]] @p @q s) return z ⇒ C of { [a] ⇒ e } -- caseπ (coe [i ⇒ [ρ. A]] @p @q s) return z ⇒ C of { [a] ⇒ e }
-- ⇝ -- ⇝
-- caseπ s ∷ [ρ. A]‹p/i› return z ⇒ C -- caseπ s ∷ [ρ. A]‹p/i› return z ⇒ C of { [a] ⇒ e[(coe [i ⇒ A] p q a)/a] }
-- of { [a] ⇒ e[(coe [i ⇒ A] p q a)/a] }
let ctx1 = extendDim i ctx let ctx1 = extendDim i ctx
Element ty tynf <- whnf defs ctx1 ty.term Element ty tynf <- whnf defs ctx1 ty.term
ta <- tycaseBOX defs ctx1 ty ta <- tycaseBOX defs ctx1 ty
@ -110,9 +109,8 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
||| pushes a coercion inside a whnf-ed term ||| pushes a coercion inside a whnf-ed term
export covering export covering
pushCoe : BindName -> pushCoe : BindName ->
(ty : Term (S d) n) -> (ty : Term (S d) n) -> (p, q : Dim d) -> (s : Term d n) -> Loc ->
(p, q : Dim d) -> (0 npq : Not (p `Eqv` q)) => (0 pc : So (canPushCoe ty s)) =>
(s : Term d n) -> (0 pc : So (canPushCoe ty s)) => Loc ->
Eff Whnf (NonRedex Elim d n defs) Eff Whnf (NonRedex Elim d n defs)
pushCoe i ty p q s loc = pushCoe i ty p q s loc =
case ty of case ty of