From b556c2f099150077f2087c3f561a20964e2accb0 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Sun, 12 May 2024 20:30:18 +0200 Subject: [PATCH] fix some comments --- lib/Quox/Equal.idr | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr index 741aa1f..789b49c 100644 --- a/lib/Quox/Equal.idr +++ b/lib/Quox/Equal.idr @@ -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