michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Quantitative: fixes a spelling error

Browse source
This commit is contained in:
Marko Dimjašević 2019-06-20 14:00:41 +02:00
parent 41dc0ba78d
commit 3e07764efe
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
extra/qtt/Quantitative.lagda
View file

@ -695,7 +695,7 @@ lem-case⊗ {γ} {δ} Γ {A} {B} {Ξ} =
(1# *̇ 0s , 1# * 0# ∙ A , 1# * 1# ∙ B) +̇ ((1# *̇ 0s , 1# * 1# ∙ A , 1# * 0# ∙ B) +̇ Γ *⟩ (λ x → Ξ x , 0# ∙ A , 0# ∙ B))
-- Step 1. Move the three occurences of A and B to the top-level.
-- Step 1. Move the three occurrences of A and B to the top-level.
≡⟨ trans (*⟩-zeroʳ Γ (λ x → Ξ x , 0# ∙ A)) (*⟩-zeroʳ Γ Ξ |> cong (_, 0# ∙ B))
|> cong (((1# *̇ 0s , 1# * 0# ∙ A , 1# * 1# ∙ B) +̇_) ∘ ((1# *̇ 0s , 1# * 1# ∙ A , 1# * 0# ∙ B) +̇_)) ⟩