Rename ∑ᵐᵛ -> ∑ (#304)

Addresses one item of #282

src/Axiom/Set/Sum.agda

@@ -113,8 +113,8 @@ module _ ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq B ⦄ where
   indexedSumᵐ : (A × B → Carrier) → FinMap A B → Carrier
   indexedSumᵐ f (m , _ , h) = indexedSum f (m , h)
 
-  indexedSumᵐᵛ : (B → Carrier) → FinMap A B → Carrier
-  indexedSumᵐᵛ f = indexedSumᵐ (f ∘ proj₂)
+  indexedSumᵛ : (B → Carrier) → FinMap A B → Carrier
+  indexedSumᵛ f = indexedSumᵐ (f ∘ proj₂)
 
   indexedSumᵐ-cong : {f : A × B → Carrier}
     → indexedSumᵐ f Preserves (_≡ᵉ_ on proj₁) ⟶ _≈_
@@ -156,5 +156,5 @@ module _ ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq B ⦄ where
             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
+  -- syntax indexedSumᵐ (λ a → x) m = ∑ᵐ[ a ← m ] x  -- (not used; leave for now?)
+  syntax indexedSumᵛ (λ a → x) m = ∑[ a ← m ] x

src/Ledger/Chain.lagda

@@ -77,7 +77,7 @@ data _⊢_⇀⦇_,NEWEPOCH⦈_ : NewEpochEnv → NewEpochState → Epoch → New
       open Acnt acnt
 
       trWithdrawals   = esW .EnactState.withdrawals
-      totWithdrawals  = ∑ᵐᵛ[ x ← trWithdrawals ᶠᵐ ] x
+      totWithdrawals  = ∑[ x ← trWithdrawals ᶠᵐ ] x
 
       removedGovActions = flip concatMapˢ removed λ (gaid , gaSt) →
         mapˢ (GovActionState.returnAddr gaSt ,_)

src/Ledger/GovernanceActions.lagda

@@ -329,7 +329,7 @@ data _⊢_⇀⦇_,ENACT⦈_ : EnactEnv → EnactState → GovAction → EnactSta
                 record  s { pparams = applyUpdate (s .pparams .proj₁) up , gid }
 
   Enact-Wdrl : let newWdrls = s .withdrawals ∪⁺ wdrl in
-    ∑ᵐᵛ[ x ← newWdrls ᶠᵐ ] x ≤ t
+    ∑[ x ← newWdrls ᶠᵐ ] x ≤ t
     ───────────────────────────────────────
     ⟦ gid , t , e ⟧ᵉ ⊢  s ⇀⦇ TreasuryWdrl wdrl  ,ENACT⦈
                 record  s { withdrawals  = newWdrls }

src/Ledger/GovernanceActions/Properties.agda

@@ -30,7 +30,7 @@ instance
     (ChangePParams up)       → just (-, Enact-PParams)
     Info                     → just (-, Enact-Info)
     (TreasuryWdrl wdrl) →
-      case ¿ ∑ᵐᵛ[ x ← (s .withdrawals ∪⁺ wdrl) ᶠᵐ ] x ≤ t ¿ of λ where
+      case ¿ ∑[ x ← (s .withdrawals ∪⁺ wdrl) ᶠᵐ ] x ≤ t ¿ of λ where
         (yes p)             → just (-, Enact-Wdrl p)
         (no _)              → nothing
   Computational-ENACT .completeness ⟦ _ , t , e ⟧ᵉ s action _ p
@@ -46,5 +46,5 @@ instance
   ... | .ChangePParams up       | Enact-PParams  = refl
   ... | .Info                   | Enact-Info     = refl
   ... | .TreasuryWdrl wdrl      | Enact-Wdrl p
-    rewrite dec-yes (¿ (∑ᵐᵛ[ x ← (s .withdrawals ∪⁺ wdrl) ᶠᵐ ] x) ≤ t ¿) p .proj₂
+    rewrite dec-yes (¿ (∑[ x ← (s .withdrawals ∪⁺ wdrl) ᶠᵐ ] x) ≤ t ¿) p .proj₂
     = refl

src/Ledger/Ratify.lagda

@@ -179,24 +179,24 @@ mostStakeDRepDist-0 = (proj₂ ∘ Equivalence.from ∈-filter)
 
 -- TODO: maybe this can be proven easier with the maximum?
 mostStakeDRepDist-∅ : ∀ {dist} → ∃[ N ] mostStakeDRepDist dist N ˢ ≡ᵉ ∅
-mostStakeDRepDist-∅ {dist} = suc (∑ᵐᵛ[ x ← dist ᶠᵐ ] x) , Properties.∅-least
+mostStakeDRepDist-∅ {dist} = suc (∑[ x ← dist ᶠᵐ ] x) , Properties.∅-least
   (⊥-elim ∘ uncurry helper ∘ Equivalence.from ∈-filter)
   where
     open ≤-Reasoning
 
-    helper : ∀ {k v} → v > ∑ᵐᵛ[ x ← dist ᶠᵐ ] x → (k , v) ∉ dist
+    helper : ∀ {k v} → v > ∑[ x ← dist ᶠᵐ ] x → (k , v) ∉ dist
     helper {k} {v} v>sum kv∈dist = 1+n≰n $ begin-strict
       v
         ≡˘⟨ indexedSum-singleton' $ finiteness ❴ k , v ❵ ⟩
-      ∑ᵐᵛ[ x ← ❴ k , v ❵ᵐ ᶠᵐ ] x
+      ∑[ x ← ❴ k , v ❵ᵐ ᶠᵐ ] x
         ≡˘⟨ indexedSumᵐ-cong {x = (dist ∣ ❴ k ❵) ᶠᵐ} {y = ❴ k , v ❵ᵐ ᶠᵐ}
           $ res-singleton' {m = dist} kv∈dist ⟩
-      ∑ᵐᵛ[ x ← (dist ∣ ❴ k ❵) ᶠᵐ ] x
+      ∑[ x ← (dist ∣ ❴ k ❵) ᶠᵐ ] x
         ≤⟨ m≤m+n _ _ ⟩
-      ∑ᵐᵛ[ x ← (dist ∣ ❴ k ❵) ᶠᵐ ] x +ℕ ∑ᵐᵛ[ x ← (dist ∣ ❴ k ❵ ᶜ) ᶠᵐ ] x
+      ∑[ x ← (dist ∣ ❴ k ❵) ᶠᵐ ] x +ℕ ∑[ x ← (dist ∣ ❴ k ❵ ᶜ) ᶠᵐ ] x
         ≡˘⟨ indexedSumᵐ-partition {m = dist ᶠᵐ} {(dist ∣ ❴ k ❵) ᶠᵐ} {(dist ∣ ❴ k ❵ ᶜ) ᶠᵐ}
           $ res-ex-disj-∪ Properties.Dec-∈-singleton ⟩
-      ∑ᵐᵛ[ x ← dist ᶠᵐ ] x
+      ∑[ x ← dist ᶠᵐ ] x
         <⟨ v>sum ⟩
       v ∎
 
@@ -344,7 +344,7 @@ abstract
   -- unused, keep until we know for sure that there'll be no minimum AVS
   -- activeVotingStake : ℙ VDeleg → StakeDistrs → (VDeleg ⇀ Vote) → Coin
   -- activeVotingStake cc dists votes =
-  --   ∑ᵐᵛ[ x  ← getStakeDist DRep cc dists ∣ dom votes ᶜ ᶠᵐ ] x
+  --   ∑[ x  ← getStakeDist DRep cc dists ∣ dom votes ᶜ ᶠᵐ ] x
 
   -- TODO: explain this notation in the prose and it's purpose:
   -- if there's no stake, accept only if threshold is zero
@@ -362,8 +362,8 @@ abstract
   acceptedStakeRatio r cc dists votes = acceptedStake /₀ totalStake
     where
       acceptedStake totalStake : Coin
-      acceptedStake = ∑ᵐᵛ[ x ← (getStakeDist r cc dists ∣ votedYesHashes votes r) ᶠᵐ ]      x
-      totalStake    = ∑ᵐᵛ[ x ←  getStakeDist r cc dists ∣ votedAbstainHashes votes r ᶜ ᶠᵐ ] x
+      acceptedStake = ∑[ x ← (getStakeDist r cc dists ∣ votedYesHashes votes r) ᶠᵐ ]      x
+      totalStake    = ∑[ x ←  getStakeDist r cc dists ∣ votedAbstainHashes votes r ᶜ ᶠᵐ ] x
 
   acceptedBy : RatifyEnv → EnactState → GovActionState → GovRole → Set
   acceptedBy Γ (record { cc = cc , _; pparams = pparams , _ }) gs role =

src/Ledger/Utxo.lagda

@@ -30,7 +30,7 @@ instance
   _ = ExUnit-CommutativeMonoid
 
   HasCoin-Map : ∀ {A} → ⦃ DecEq A ⦄ → HasCoin (A ⇀ Coin)
-  HasCoin-Map .getCoin s = indexedSumᵐᵛ ⦃ +-0-commutativeMonoid ⦄ id (s ᶠᵐ)
+  HasCoin-Map .getCoin s = indexedSumᵛ ⦃ +-0-commutativeMonoid ⦄ id (s ᶠᵐ)
 
 isPhaseTwoScriptAddress : Tx → Addr → Bool
 isPhaseTwoScriptAddress tx a
@@ -79,7 +79,7 @@ module _ (let open Tx; open TxBody) where
   outs tx = mapKeys (tx .txid ,_) (tx .txouts)
 
   balance : UTxO → Value
-  balance utxo = indexedSumᵐᵛ ⦃ Value-CommutativeMonoid ⦄ getValue (utxo ᶠᵐ)
+  balance utxo = indexedSumᵛ ⦃ Value-CommutativeMonoid ⦄ getValue (utxo ᶠᵐ)
 
   cbalance : UTxO → Coin
   cbalance utxo = coin (balance utxo)