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

fix quantity in CasePair typing

Browse source
This commit is contained in:
rhiannon morris 2023-02-23 10:04:00 +01:00
parent abe812fc40
commit 4b814d7502
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
lib/Quox/Typechecker.idr
View file

@ -235,10 +235,11 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
(tfst, tsnd) <- expectSig !ask pairres.type (tfst, tsnd) <- expectSig !ask pairres.type
-- if Ψ | Γ, x : A, y : B ⊢ σ · body ⇐ -- if Ψ | Γ, x : A, y : B ⊢ σ · body ⇐
-- ret[(x, y) ∷ (x : A) × B/p] ⊳ Σ₂, ρ₁·x, ρ₂·y -- ret[(x, y) ∷ (x : A) × B/p] ⊳ Σ₂, ρ₁·x, ρ₂·y
-- with ρ₁, ρ₂ ≤ π -- with ρ₁, ρ₂ ≤ πσ
let bodyctx = extendTyN [< tfst, tsnd.term] ctx let bodyctx = extendTyN [< tfst, tsnd.term] ctx
bodyty = substCasePairRet pairres.type ret bodyty = substCasePairRet pairres.type ret
bodyout <- popQs [< pi, pi] !(checkC bodyctx sg body.term bodyty) pisg = pi * sg.fst
bodyout <- popQs [< pisg, pisg] !(checkC bodyctx sg body.term bodyty)
-- then Ψ | Γ ⊢ σ · case ⋯ ⇒ ret[pair/p] ⊳ πΣ₁ + Σ₂ -- then Ψ | Γ ⊢ σ · case ⋯ ⇒ ret[pair/p] ⊳ πΣ₁ + Σ₂
pure $ InfRes { pure $ InfRes {
type = sub1 ret pair, type = sub1 ret pair,