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

fix some comments

Browse source
This commit is contained in:
rhiannon morris 2024-05-12 20:30:18 +02:00
parent d2a117fe61
commit b556c2f099
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
lib/Quox/Equal.idr
View file

@ -249,18 +249,18 @@ namespace Term
compare0' defs ctx sg ty@(Pi {qty, arg, res, _}) s t = withEqual $
-- Γ ⊢ A empty
-- -------------------------------------------
-- Γ ⊢ (λ x ⇒ s) = (λ x ⇒ t) ⇐ (π·x : A) → B
-- Γ ⊢ (λ x ⇒ s) = (λ x ⇒ t) ⇐ π.(x : A) → B
if !(isEmpty defs ctx sg arg) then pure () else
case (s, t) of
-- Γ, x : A ⊢ s = t ⇐ B
-- -------------------------------------------
-- Γ ⊢ (λ x ⇒ s) = (λ x ⇒ t) ⇐ (π·x : A) → B
-- Γ ⊢ (λ x ⇒ s) = (λ x ⇒ t) ⇐ π.(x : A) → B
(Lam b1 {}, Lam b2 {}) =>
compare0 defs ctx' sg res.term b1.term b2.term
-- Γ, x : A ⊢ s = e x ⇐ B
-- -----------------------------------
-- Γ ⊢ (λ x ⇒ s) = e ⇐ (π·x : A) → B
-- Γ ⊢ (λ x ⇒ s) = e ⇐ π.(x : A) → B
(E e, Lam b {}) => eta s.loc e b
(Lam b {}, E e) => eta s.loc e b
@ -435,7 +435,7 @@ compareType' defs ctx (Pi {qty = sQty, arg = sArg, res = sRes, loc})
(Pi {qty = tQty, arg = tArg, res = tRes, _}) = do
-- Γ ⊢ A₁ :> A₂ Γ, x : A₁ ⊢ B₁ <: B₂
-- ----------------------------------------
-- Γ ⊢ (π·x : A₁) → B₁ <: (π·x : A₂) → B₂
-- Γ ⊢ π.(x : A₁) → B₁ <: π.(x : A₂) → B₂
expectEqualQ loc sQty tQty
local flip $ compareType defs ctx sArg tArg -- contra
compareType defs (extendTy0 sRes.name sArg ctx) sRes.term tRes.term