From 3abc6be135ea11b99cbf87edf1ee8a09ce97e1a9 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Wed, 18 Oct 2023 14:40:52 -0600 Subject: [PATCH] PDF cleanup: rename union symbol MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Address the following items (the first from #146, the second a consequence of the first): + [X] Rename `∪ᵐˡ` to `∪ˡ` + [X] adjust alignment affected by union renaming --- src/Axiom/Set/Map.agda | 18 ++++++------- src/Axiom/Set/Sum.agda | 26 +++++++++--------- src/Ledger/Deleg.lagda | 8 +++--- src/Ledger/GovernanceActions.lagda | 2 +- src/Ledger/PPUp.lagda | 4 +-- src/Ledger/Ratify.lagda | 22 ++++++++-------- src/Ledger/Utxo.lagda | 2 +- src/Ledger/Utxo/Properties.lagda | 42 +++++++++++++++--------------- src/latex/agda-latex-macros.sty | 2 +- 9 files changed, 63 insertions(+), 63 deletions(-) diff --git a/src/Axiom/Set/Map.agda b/src/Axiom/Set/Map.agda index 347f94dba..f5d996aab 100644 --- a/src/Axiom/Set/Map.agda +++ b/src/Axiom/Set/Map.agda @@ -153,22 +153,22 @@ singletonᵐ a b = ❴ (a , b) ❵ ❴ k , v ❵ᵐ = singletonᵐ k v module Unionᵐ (sp-∈ : spec-∈ A) where - infixr 6 _∪ᵐˡ_ + infixr 6 _∪ˡ_ - _∪ᵐˡ'_ : Rel A B → Rel A B → Rel A B - m ∪ᵐˡ' m' = m ∪ filter (sp-∘ (sp-¬ (sp-∈ {dom m})) proj₁) m' + _∪ˡ'_ : Rel A B → Rel A B → Rel A B + m ∪ˡ' m' = m ∪ filter (sp-∘ (sp-¬ (sp-∈ {dom m})) proj₁) m' - _∪ᵐˡ_ : Map A B → Map A B → Map A B - m ∪ᵐˡ m' = disj-∪ m (filterᵐ (sp-∘ (sp-¬ sp-∈) proj₁) m') + _∪ˡ_ : Map A B → Map A B → Map A B + m ∪ˡ m' = disj-∪ m (filterᵐ (sp-∘ (sp-¬ sp-∈) proj₁) m') (∈⇔P -⟨ (λ where x (_ , refl , hy) → proj₁ (∈⇔P hy) (∈⇔P x)) ⟩- ∈⇔P) - disjoint-∪ᵐˡ-∪ : (H : disjoint (dom R) (dom R')) → R ∪ᵐˡ' R' ≡ᵉ R ∪ R' - disjoint-∪ᵐˡ-∪ disj = from ≡ᵉ⇔≡ᵉ' λ _ → mk⇔ + disjoint-∪ˡ-∪ : (H : disjoint (dom R) (dom R')) → R ∪ˡ' R' ≡ᵉ R ∪ R' + disjoint-∪ˡ-∪ disj = from ≡ᵉ⇔≡ᵉ' λ _ → mk⇔ (∈-∪⁺ ∘′ map₂ (proj₂ ∘′ ∈⇔P) ∘′ ∈⇔P) (∈⇔P ∘′ map₂ (to ∈-filter ∘′ (λ h → (flip disj (∈-map⁺'' h)) , h)) ∘ ∈⇔P) insert : Map A B → A → B → Map A B - insert m a b = ❴ a , b ❵ᵐ ∪ᵐˡ m + insert m a b = ❴ a , b ❵ᵐ ∪ˡ m insertIfJust : ⦃ DecEq A ⦄ → A → Maybe B → Map A B → Map A B insertIfJust x nothing m = m @@ -281,7 +281,7 @@ module Restrictionᵐ (sp-∈ : spec-∈ A) where -- map only values in X mapValueRestricted : (B → B) → Map A B → Set A → Map A B - mapValueRestricted f m X = mapValues f (m ∣ X) ∪ᵐˡ m + mapValueRestricted f m X = mapValues f (m ∣ X) ∪ˡ m -- map only value at a mapSingleValue : (B → B) → Map A B → A → Map A B diff --git a/src/Axiom/Set/Sum.agda b/src/Axiom/Set/Sum.agda index f7c224a66..8d5158f5a 100644 --- a/src/Axiom/Set/Sum.agda +++ b/src/Axiom/Set/Sum.agda @@ -125,20 +125,20 @@ module _ ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq B ⦄ where open Unionᵐ sp-∈ - ∪ᵐˡ-finite : {R R' : Rel A B} → finite R → finite R' → finite (R ∪ᵐˡ' R') - ∪ᵐˡ-finite Rᶠ R'ᶠ = ∪-preserves-finite Rᶠ + ∪ˡ-finite : {R R' : Rel A B} → finite R → finite R' → finite (R ∪ˡ' R') + ∪ˡ-finite Rᶠ R'ᶠ = ∪-preserves-finite Rᶠ $ filter-finite (sp-∘ (sp-¬ sp-∈) _) (¬? ∘ ∈-A-dec ∘ _) R'ᶠ - _∪ᵐˡᶠ_ : FinMap A B → FinMap A B → FinMap A B - (_ , hX , Xᶠ) ∪ᵐˡᶠ (_ , hY , Yᶠ) = - toFinMap ((_ , hX) ∪ᵐˡ (_ , hY)) (∪ᵐˡ-finite Xᶠ Yᶠ) + _∪ˡᶠ_ : FinMap A B → FinMap A B → FinMap A B + (_ , hX , Xᶠ) ∪ˡᶠ (_ , hY , Yᶠ) = + toFinMap ((_ , hX) ∪ˡ (_ , hY)) (∪ˡ-finite Xᶠ Yᶠ) indexedSumᵐ-∪ : ∀ {X Y : FinMap A B} {f} → disjoint (dom (toRel X)) (dom (toRel Y)) - → indexedSumᵐ f (X ∪ᵐˡᶠ Y) ≈ indexedSumᵐ f X ∙ indexedSumᵐ f Y + → indexedSumᵐ f (X ∪ˡᶠ Y) ≈ indexedSumᵐ f X ∙ indexedSumᵐ f Y indexedSumᵐ-∪ {X = X'@(X , _ , Xᶠ)} {Y'@(Y , _ , Yᶠ)} {f} disj = begin - indexedSumᵐ f (X' ∪ᵐˡᶠ Y') ≈⟨ indexedSum-cong {x = -, ∪ᵐˡ-finite Xᶠ Yᶠ} {(X ∪ Y) ᶠ} - $ disjoint-∪ᵐˡ-∪ disj ⟩ + indexedSumᵐ f (X' ∪ˡᶠ Y') ≈⟨ indexedSum-cong {x = -, ∪ˡ-finite Xᶠ Yᶠ} {(X ∪ Y) ᶠ} + $ disjoint-∪ˡ-∪ disj ⟩ indexedSum f ((X ∪ Y) ᶠ) ≈⟨ indexedSum-∪ (disjoint-dom⇒disjoint disj) ⟩ indexedSumᵐ f X' ∙ indexedSumᵐ f Y' ∎ where instance _ = Xᶠ @@ -147,14 +147,14 @@ module _ ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq B ⦄ where indexedSumᵐ-partition : ∀ {m m₁ m₂ : FinMap A B} {f} → toRel m ≡ toRel m₁ ⨿ toRel m₂ → indexedSumᵐ f m ≈ indexedSumᵐ f m₁ ∙ indexedSumᵐ f m₂ indexedSumᵐ-partition {m} {m₁} {m₂} {f} m≡m₁∪m₂ = begin - indexedSumᵐ f m ≈⟨ indexedSumᵐ-cong {x = m} {m₁ ∪ᵐˡᶠ m₂} helper ⟩ - indexedSumᵐ f (m₁ ∪ᵐˡᶠ m₂) ≈⟨ indexedSumᵐ-∪ {X = m₁} {Y = m₂} disj-dom' ⟩ - indexedSumᵐ f m₁ ∙ indexedSumᵐ f m₂ ∎ + indexedSumᵐ f m ≈⟨ indexedSumᵐ-cong {x = m} {m₁ ∪ˡᶠ m₂} helper ⟩ + indexedSumᵐ f (m₁ ∪ˡᶠ m₂) ≈⟨ indexedSumᵐ-∪ {X = m₁} {Y = m₂} disj-dom' ⟩ + indexedSumᵐ f m₁ ∙ indexedSumᵐ f m₂ ∎ where module ≡ᵉ = IsEquivalence ≡ᵉ-isEquivalence disj-dom' = disj-dom {m = toMap m} {toMap m₁} {toMap m₂} m≡m₁∪m₂ - helper : toRel m ≡ᵉ toRel (m₁ ∪ᵐˡᶠ m₂) - helper = ≡ᵉ.trans (proj₁ m≡m₁∪m₂) (≡ᵉ.sym $ disjoint-∪ᵐˡ-∪ disj-dom') + helper : toRel m ≡ᵉ toRel (m₁ ∪ˡᶠ m₂) + helper = ≡ᵉ.trans (proj₁ m≡m₁∪m₂) (≡ᵉ.sym $ disjoint-∪ˡ-∪ disj-dom') syntax indexedSumᵐ (λ a → x) m = Σᵐ[ a ← m ] x syntax indexedSumᵐᵛ (λ a → x) m = Σᵐᵛ[ a ← m ] x diff --git a/src/Ledger/Deleg.lagda b/src/Ledger/Deleg.lagda index 7d36caab0..baf90e300 100644 --- a/src/Ledger/Deleg.lagda +++ b/src/Ledger/Deleg.lagda @@ -123,18 +123,18 @@ data _⊢_⇀⦇_,POOL⦈_ : PoolEnv → PState → DCert → PState → Set whe c ∉ dom pools ──────────────────────────────── pp ⊢ ⟦ pools , retiring ⟧ᵖ ⇀⦇ regpool c poolParams ,POOL⦈ - ⟦ ❴ c , poolParams ❵ᵐ ∪ᵐˡ pools , retiring ⟧ᵖ + ⟦ ❴ c , poolParams ❵ᵐ ∪ˡ pools , retiring ⟧ᵖ POOL-retirepool : pp ⊢ ⟦ pools , retiring ⟧ᵖ ⇀⦇ retirepool c e ,POOL⦈ - ⟦ pools , ❴ c , e ❵ᵐ ∪ᵐˡ retiring ⟧ᵖ + ⟦ pools , ❴ c , e ❵ᵐ ∪ˡ retiring ⟧ᵖ data _⊢_⇀⦇_,GOVCERT⦈_ : GovCertEnv → GState → DCert → GState → Set where GOVCERT-regdrep : let open PParams pp in (d ≡ drepDeposit × c ∉ dom dReps) ⊎ (d ≡ 0 × c ∈ dom dReps) ──────────────────────────────── ⟦ e , pp , vs ⟧ᶜ ⊢ ⟦ dReps , ccKeys ⟧ᵛ ⇀⦇ regdrep c d an ,GOVCERT⦈ - ⟦ ❴ c , e + drepActivity ❵ᵐ ∪ᵐˡ dReps , ccKeys ⟧ᵛ + ⟦ ❴ c , e + drepActivity ❵ᵐ ∪ˡ dReps , ccKeys ⟧ᵛ GOVCERT-deregdrep : c ∈ dom dReps @@ -146,7 +146,7 @@ data _⊢_⇀⦇_,GOVCERT⦈_ : GovCertEnv → GState → DCert → GState → S (c , nothing) ∉ ccKeys ──────────────────────────────── Γ ⊢ ⟦ dReps , ccKeys ⟧ᵛ ⇀⦇ ccreghot c mc ,GOVCERT⦈ - ⟦ dReps , singletonᵐ c mc ∪ᵐˡ ccKeys ⟧ᵛ + ⟦ dReps , singletonᵐ c mc ∪ˡ ccKeys ⟧ᵛ \end{code} \caption{Auxiliary DELEG and POOL rules} \end{figure*} diff --git a/src/Ledger/GovernanceActions.lagda b/src/Ledger/GovernanceActions.lagda index 7f6cd7963..be82f43b3 100644 --- a/src/Ledger/GovernanceActions.lagda +++ b/src/Ledger/GovernanceActions.lagda @@ -322,7 +322,7 @@ data _⊢_⇀⦇_,ENACT⦈_ : EnactEnv → EnactState → GovAction → EnactSta ∀[ term ∈ range new ] term ≤ (s .pparams .proj₁ .PParams.ccMaxTermLength +ᵉ e) ──────────────────────────────── ⟦ gid , t , e ⟧ᵉ ⊢ s ⇀⦇ NewCommittee new rem q ,ENACT⦈ - record s { cc = just ((new ∪ᵐˡ old) ∣ rem ᶜ , q) , gid } + record s { cc = just ((new ∪ˡ old) ∣ rem ᶜ , q) , gid } Enact-NewConst : ⟦ gid , t , e ⟧ᵉ ⊢ s ⇀⦇ NewConstitution dh sh ,ENACT⦈ diff --git a/src/Ledger/PPUp.lagda b/src/Ledger/PPUp.lagda index e17e43a25..d12f2d76c 100644 --- a/src/Ledger/PPUp.lagda +++ b/src/Ledger/PPUp.lagda @@ -95,7 +95,7 @@ data _⊢_⇀⦇_,PPUP⦈_ : PPUpdateEnv → PPUpdateState → Maybe Update → → epoch slot ≡ e ──────────────────────────────── Γ ⊢ record { pup = pupˢ ; fpup = fpupˢ } ⇀⦇ just (pup , e) ,PPUP⦈ - record { pup = pup ∪ᵐˡ pupˢ ; fpup = fpupˢ } + record { pup = pup ∪ˡ pupˢ ; fpup = fpupˢ } PPUpdateFuture : let open PPUpdateEnv Γ in dom pup ⊆ dom genDelegs @@ -104,7 +104,7 @@ data _⊢_⇀⦇_,PPUP⦈_ : PPUpdateEnv → PPUpdateState → Maybe Update → → sucᵉ (epoch slot) ≡ e ──────────────────────────────── Γ ⊢ record { pup = pupˢ ; fpup = fpupˢ } ⇀⦇ just (pup , e) ,PPUP⦈ - record { pup = pupˢ ; fpup = pup ∪ᵐˡ fpupˢ } + record { pup = pupˢ ; fpup = pup ∪ˡ fpupˢ } \end{code} \caption{PPUP inference rules} \end{figure*} diff --git a/src/Ledger/Ratify.lagda b/src/Ledger/Ratify.lagda index 0f26b2049..e92d8a8c5 100644 --- a/src/Ledger/Ratify.lagda +++ b/src/Ledger/Ratify.lagda @@ -229,7 +229,7 @@ restrictedDists coins rank dists = dists where open StakeDistrs dists -- one always includes the other restrict : Credential ⇀ Coin → Credential ⇀ Coin - restrict dist = topNDRepDist rank dist ∪ᵐˡ mostStakeDRepDist dist coins + restrict dist = topNDRepDist rank dist ∪ˡ mostStakeDRepDist dist coins \end{code} \begin{figure*}[h!] {\small @@ -237,9 +237,9 @@ restrictedDists coins rank dists = dists actualVotes : RatifyEnv → CCData → (GovRole × Credential) ⇀ Vote → GovAction → PParams → VDeleg ⇀ Vote actualVotes Γ cc votes ga pparams - = mapKeys (credVoter CC) actualCCVotes - ∪ᵐˡ actualPDRepVotes ∪ᵐˡ actualDRepVotes - ∪ᵐˡ actualSPOVotes + = mapKeys (credVoter CC) actualCCVotes + ∪ˡ actualPDRepVotes ∪ˡ actualDRepVotes + ∪ˡ actualSPOVotes where open RatifyEnv Γ open PParams pparams @@ -267,17 +267,17 @@ actualVotes Γ cc votes ga pparams (nothing , _) → ∅ᵐ actualPDRepVotes - = ❴ abstainRep , Vote.abstain ❵ᵐ - ∪ᵐˡ ❴ noConfidenceRep , (case ga of λ where NoConfidence → Vote.yes - _ → Vote.no) ❵ᵐ + = ❴ abstainRep , Vote.abstain ❵ᵐ + ∪ˡ ❴ noConfidenceRep , (case ga of λ where NoConfidence → Vote.yes + _ → Vote.no) ❵ᵐ actualDRepVotes - = roleVotes GovRole.DRep - ∪ᵐˡ constMap (mapˢ (credVoter DRep) activeDReps) Vote.no + = roleVotes GovRole.DRep + ∪ˡ constMap (mapˢ (credVoter DRep) activeDReps) Vote.no actualSPOVotes - = roleVotes GovRole.SPO - ∪ᵐˡ constMap spos (if isHF then Vote.no else Vote.abstain) + = roleVotes GovRole.SPO + ∪ˡ constMap spos (if isHF then Vote.no else Vote.abstain) where spos : ℙ VDeleg spos = filterˢ isSPOProp $ dom (StakeDistrs.stakeDistr stakeDistrs) diff --git a/src/Ledger/Utxo.lagda b/src/Ledger/Utxo.lagda index a1f966b33..43ea48ee2 100644 --- a/src/Ledger/Utxo.lagda +++ b/src/Ledger/Utxo.lagda @@ -319,7 +319,7 @@ data _⊢_⇀⦇_,UTXO⦈_ where -- Add deposits ──────────────────────────────── - Γ ⊢ s ⇀⦇ tx ,UTXO⦈ ⟦ (utxo ∣ txins ᶜ) ∪ᵐˡ (outs txb) + Γ ⊢ s ⇀⦇ tx ,UTXO⦈ ⟦ (utxo ∣ txins ᶜ) ∪ˡ outs txb , fees + txfee , updateDeposits pp txb deposits , donations + txdonation diff --git a/src/Ledger/Utxo/Properties.lagda b/src/Ledger/Utxo/Properties.lagda index 3df2b7de1..f951fd78b 100644 --- a/src/Ledger/Utxo/Properties.lagda +++ b/src/Ledger/Utxo/Properties.lagda @@ -60,13 +60,13 @@ private ∙-homo-Coin = IsMagmaHomomorphism.homo (isMagmaHomomorphism coinIsMonoidHomomorphism) balance-∪ : disjoint (dom utxo) (dom utxo') - → cbalance (utxo ∪ᵐˡ utxo') ≡ cbalance utxo + cbalance utxo' + → cbalance (utxo ∪ˡ utxo') ≡ cbalance utxo + cbalance utxo' balance-∪ {utxo} {utxo'} h = begin - cbalance (utxo ∪ᵐˡ utxo') + cbalance (utxo ∪ˡ utxo') ≡⟨ ⟦⟧-cong coinIsMonoidHomomorphism - $ indexedSumᵐ-cong {x = (utxo ∪ᵐˡ utxo') ᶠᵐ} {(utxo ᶠᵐ) ∪ᵐˡᶠ (utxo' ᶠᵐ)} (id , id) + $ indexedSumᵐ-cong {x = (utxo ∪ˡ utxo') ᶠᵐ} {(utxo ᶠᵐ) ∪ˡᶠ (utxo' ᶠᵐ)} (id , id) ⟩ - coin (indexedSumᵐ _ ((utxo ᶠᵐ) ∪ᵐˡᶠ (utxo' ᶠᵐ))) + coin (indexedSumᵐ _ ((utxo ᶠᵐ) ∪ˡᶠ (utxo' ᶠᵐ))) ≡⟨ ⟦⟧-cong coinIsMonoidHomomorphism $ indexedSumᵐ-∪ {X = utxo ᶠᵐ} {utxo' ᶠᵐ} h ⟩ @@ -249,15 +249,15 @@ module DepositHelpers utxo-ref-prop : cbalance utxo + ref ≡ - (cbalance ((utxo ∣ txins ᶜ) ∪ᵐˡ outs txb) + txfee) + txdonation + tot + (cbalance ((utxo ∣ txins ᶜ) ∪ˡ outs txb) + txfee) + txdonation + tot utxo-ref-prop = begin cbalance utxo + ref ≡˘⟨ cong (_+ ref) - $ balance-cong-coin {utxo = (utxo ∣ txins ᶜ) ∪ᵐˡ (utxo ∣ txins)}{utxo} - $ disjoint-∪ᵐˡ-∪ (disjoint-sym res-ex-disjoint) + $ balance-cong-coin {utxo = (utxo ∣ txins ᶜ) ∪ˡ (utxo ∣ txins)}{utxo} + $ disjoint-∪ˡ-∪ (disjoint-sym res-ex-disjoint) ≡ᵉ-∘ ∪-sym ≡ᵉ-∘ res-ex-∪ (_∈? txins) ⟩ - cbalance ((utxo ∣ txins ᶜ) ∪ᵐˡ (utxo ∣ txins)) + ref + cbalance ((utxo ∣ txins ᶜ) ∪ˡ (utxo ∣ txins)) + ref ≡⟨ cong (_+ ref) $ balance-∪ {utxo ∣ txins ᶜ} {utxo ∣ txins} $ flip res-ex-disjoint ⟩ @@ -273,17 +273,17 @@ module DepositHelpers ℕ.+ tot ℕ.+ txdonation ≡˘⟨ cong (λ x → (x + txfee) + tot + txdonation) $ balance-∪ {utxo ∣ txins ᶜ} {outs txb} h ⟩ - (cbalance ((utxo ∣ txins ᶜ) ∪ᵐˡ outs txb) ℕ.+ txfee) + (cbalance ((utxo ∣ txins ᶜ) ∪ˡ outs txb) ℕ.+ txfee) ℕ.+ tot ℕ.+ txdonation ≡t⟨⟩ - (cbalance ((utxo ∣ txins ᶜ) ∪ᵐˡ outs txb) ℕ.+ txfee) + (cbalance ((utxo ∣ txins ᶜ) ∪ˡ outs txb) ℕ.+ txfee) ℕ.+ (tot ℕ.+ txdonation) - ≡⟨ cong ((cbalance ((utxo ∣ txins ᶜ) ∪ᵐˡ outs txb) + txfee) +_) + ≡⟨ cong ((cbalance ((utxo ∣ txins ᶜ) ∪ˡ outs txb) + txfee) +_) $ +-comm tot txdonation ⟩ - (cbalance ((utxo ∣ txins ᶜ) ∪ᵐˡ outs txb) ℕ.+ txfee) + (cbalance ((utxo ∣ txins ᶜ) ∪ˡ outs txb) ℕ.+ txfee) ℕ.+ (txdonation ℕ.+ tot) ≡t⟨⟩ - (cbalance ((utxo ∣ txins ᶜ) ∪ᵐˡ outs txb) ℕ.+ txfee) + (cbalance ((utxo ∣ txins ᶜ) ∪ˡ outs txb) ℕ.+ txfee) ℕ.+ txdonation ℕ.+ tot ∎ where open IsEquivalence ≡ᵉ-isEquivalence renaming (trans to infixl 4 _≡ᵉ-∘_) @@ -380,24 +380,24 @@ pov {tx}{utxo}{_}{fees}{deposits}{donations} ≡t⟨⟩ cbalance utxo ℕ.+ ref ℕ.+ (remDepTot ℕ.+ fees) ≡⟨ cong (_+ (remDepTot + fees)) utxo-ref-prop ⟩ - (cbalance ((utxo ∣ txins ᶜ) ∪ᵐˡ outs txb) ℕ.+ txfee) + (cbalance ((utxo ∣ txins ᶜ) ∪ˡ outs txb) ℕ.+ txfee) ℕ.+ txdonation ℕ.+ tot ℕ.+ (remDepTot ℕ.+ fees) ≡t⟨⟩ - cbalance ((utxo ∣ txins ᶜ) ∪ᵐˡ outs txb) + cbalance ((utxo ∣ txins ᶜ) ∪ˡ outs txb) ℕ.+ (txfee ℕ.+ txdonation ℕ.+ (tot ℕ.+ remDepTot) ℕ.+ fees) - ≡⟨ cong (cbalance ((utxo ∣ txins ᶜ) ∪ᵐˡ outs txb) +_) rearrange0 ⟩ - cbalance ((utxo ∣ txins ᶜ) ∪ᵐˡ outs txb) + ≡⟨ cong (cbalance ((utxo ∣ txins ᶜ) ∪ˡ outs txb) +_) rearrange0 ⟩ + cbalance ((utxo ∣ txins ᶜ) ∪ˡ outs txb) + ((fees + txfee) + getCoin deposits' + txdonation) ∎ ⟩ - cbalance ((utxo ∣ txins ᶜ) ∪ᵐˡ outs txb) + cbalance ((utxo ∣ txins ᶜ) ∪ˡ outs txb) ℕ.+ ((fees + txfee) ℕ.+ getCoin deposits' ℕ.+ txdonation) ℕ.+ donations ≡t⟨⟩ - cbalance ((utxo ∣ txins ᶜ) ∪ᵐˡ outs txb) + cbalance ((utxo ∣ txins ᶜ) ∪ˡ outs txb) ℕ.+ (fees + txfee) ℕ.+ getCoin deposits' ℕ.+ (txdonation ℕ.+ donations) - ≡⟨ cong (cbalance ((utxo ∣ txins ᶜ) ∪ᵐˡ outs txb) + ≡⟨ cong (cbalance ((utxo ∣ txins ᶜ) ∪ˡ outs txb) + (fees + txfee) + getCoin deposits' ℕ.+_) $ +-comm txdonation donations ⟩ - cbalance ((utxo ∣ txins ᶜ) ∪ᵐˡ outs txb) + cbalance ((utxo ∣ txins ᶜ) ∪ˡ outs txb) + (fees + txfee) + getCoin deposits' + (donations + txdonation) ∎ \end{code} diff --git a/src/latex/agda-latex-macros.sty b/src/latex/agda-latex-macros.sty index a22c880c2..dc4832a30 100644 --- a/src/latex/agda-latex-macros.sty +++ b/src/latex/agda-latex-macros.sty @@ -177,7 +177,7 @@ \newcommand{\Credential}{\AgdaFunction{Credential}\xspace} \newcommand{\credVoter}{\AgdaInductiveConstructor{credVoter}\xspace} \newcommand{\Crypto}{\AgdaRecord{Crypto}\xspace} -\newcommand{\cupsupermsuperl}{\AgdaFunction{∪ᵐˡ}\xspace} +\newcommand{\cupsupermsuperl}{\AgdaFunction{∪ˡ}\xspace} \newcommand{\cupsuperplus}{\AgdaFunction{∪⁺}\xspace} \newcommand{\currentEpoch}{\AgdaField{currentEpoch}\xspace}