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

fix case-box typing

Browse source
This commit is contained in:
rhiannon morris 2023-04-01 16:01:29 +02:00
parent 1fce4d80f6
commit 036e2bd4a5
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
lib/Quox/Typechecker.idr
View file

@ -407,7 +407,7 @@ parameters {auto _ : IsQty q}
-- if Ψ | Γ, x : A ⊢ t ⇐ R[[x] ∷ [ρ.A/x]] ⊳ Σ₂, ς·x -- if Ψ | Γ, x : A ⊢ t ⇐ R[[x] ∷ [ρ.A/x]] ⊳ Σ₂, ς·x
-- with ς ≤ ρπσ -- with ς ≤ ρπσ
let qpisg = q * pi * sg.fst let qpisg = q * pi * sg.fst
bodyCtx = extendTy qpisg body.name boxres.type ctx bodyCtx = extendTy qpisg body.name ty ctx
bodyType = substCaseBoxRet ty ret bodyType = substCaseBoxRet ty ret
bodyout <- checkC bodyCtx sg body.term bodyType >>= popQ qpisg bodyout <- checkC bodyCtx sg body.term bodyType >>= popQ qpisg
-- then Ψ | Γ ⊢ case ⋯ ⇒ R[b/x] ⊳ Σ₁ + Σ₂ -- then Ψ | Γ ⊢ case ⋯ ⇒ R[b/x] ⊳ Σ₁ + Σ₂