From c152845d88929d705cc7171255a6ccda49170175 Mon Sep 17 00:00:00 2001 From: Orestis Melkonian Date: Wed, 27 Sep 2023 14:12:34 +0100 Subject: [PATCH] =?UTF-8?q?Fix=20instance=20resolution=20of=20=5F=E2=89=A4?= =?UTF-8?q?=E1=B5=89=5F,=20and=20left-over=20renamings=20from=20#900a1?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Axiom/Set.agda | 6 +--- src/Axiom/Set/Map/Dec.agda | 1 - src/Axiom/Set/Rel.agda | 4 +-- src/Axiom/Set/Sum.agda | 5 +-- src/Axiom/Set/TotalMap.agda | 1 - src/Axiom/Set/TotalMapOn.agda | 1 - src/Ledger/Epoch.agda | 51 ++++++++++++++++-------------- src/Ledger/Gov.lagda | 1 - src/Ledger/GovernanceActions.lagda | 10 ++---- src/Ledger/Ledger/Properties.agda | 1 - src/Ledger/PDF.lagda | 4 --- src/Ledger/PParams.lagda | 8 ++--- src/Ledger/Prelude.agda | 4 +-- src/Ledger/Ratify.lagda | 1 - src/Ledger/Utxo.lagda | 2 +- src/Ledger/Utxow/Properties.agda | 4 +-- src/Prelude.agda | 43 ++++++++++++++++++------- src/latex/agda-latex-macros.sty | 6 ++-- 18 files changed, 80 insertions(+), 73 deletions(-) diff --git a/src/Axiom/Set.agda b/src/Axiom/Set.agda index 619cf0f2f..de7ecdcda 100644 --- a/src/Axiom/Set.agda +++ b/src/Axiom/Set.agda @@ -8,7 +8,6 @@ open import Prelude hiding (filter) import Function.Related.Propositional as R open import Data.List.Ext.Properties using (∈-dedup; _×-cong_) -open import Data.List.Membership.Propositional using () renaming (_∈_ to _∈ˡ_) open import Data.List.Relation.Unary.Any using (here; there) open import Data.List.Relation.Unary.Unique.DecPropositional.Properties using (deduplicate-!) open import Data.List.Relation.Unary.Unique.Propositional using (Unique; []) @@ -17,9 +16,6 @@ open import Data.Product.Properties using (∃∃↔∃∃) open import Data.Product.Properties.Ext using (∃-cong′; ∃-≡) open import Interface.DecEq using (DecEq; _≟_) open import Relation.Binary using () renaming (Decidable to Dec₂) -open import Relation.Nullary using (¬?; Dec; yes; no) -open import Relation.Nullary.Decidable using (⌊_⌋) -open import Relation.Unary using (Pred) renaming (Decidable to Decidable¹) private variable ℓ : Level @@ -309,7 +305,7 @@ record Theoryᵈ : Type₁ where field ∈-sp : ⦃ DecEq A ⦄ → spec-∈ A - _∈?_ : ⦃ DecEq A ⦄ → Dec₂ (_∈_ {A = A}) + _∈?_ : ⦃ DecEq A ⦄ → Decidable² (_∈_ {A = A}) all? : ⦃ DecEq A ⦄ → {P : A → Type} (P? : Decidable¹ P) {X : Set A} → Dec (All P X) any? : ⦃ DecEq A ⦄ → {P : A → Type} (P? : Decidable¹ P) (X : Set A) → Dec (Any P X) diff --git a/src/Axiom/Set/Map/Dec.agda b/src/Axiom/Set/Map/Dec.agda index cb4b925ec..aef2e8854 100644 --- a/src/Axiom/Set/Map/Dec.agda +++ b/src/Axiom/Set/Map/Dec.agda @@ -10,7 +10,6 @@ open import Algebra using (Monoid) import Data.Sum as Sum open import Data.These hiding (map) open import Interface.DecEq using (DecEq) -open import Relation.Nullary.Decidable using (yes; no) open Theoryᵈ thᵈ using (_∈?_; th; incl-set'; incl-set) open Theory th diff --git a/src/Axiom/Set/Rel.agda b/src/Axiom/Set/Rel.agda index a571494c3..bfa7311d2 100644 --- a/src/Axiom/Set/Rel.agda +++ b/src/Axiom/Set/Rel.agda @@ -1,6 +1,8 @@ {-# OPTIONS --safe --no-import-sorts #-} {-# OPTIONS -v allTactics:100 #-} +open import Prelude hiding (filter) + open import Agda.Primitive using (lzero) renaming (Set to Type) open import Axiom.Set using (Theory) @@ -12,8 +14,6 @@ import Function.Related.Propositional as R open Theory th open import Axiom.Set.Properties th -open import Prelude hiding (filter) - import Data.Product open import Data.These hiding (map) open import Data.Maybe.Base using () renaming (map to map?) diff --git a/src/Axiom/Set/Sum.agda b/src/Axiom/Set/Sum.agda index 8c872892c..f7c224a66 100644 --- a/src/Axiom/Set/Sum.agda +++ b/src/Axiom/Set/Sum.agda @@ -19,7 +19,6 @@ open import Data.List.Relation.Binary.Permutation.Propositional open import Data.List.Relation.Unary.Unique.Propositional using (Unique) open import Interface.DecEq using (DecEq; _≟_) open import Relation.Binary using (_Preserves_⟶_; IsEquivalence) -open import Relation.Nullary.Decidable using (¬?) open import Relation.Unary using (Decidable) open import Tactic.AnyOf @@ -121,7 +120,9 @@ module _ ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq B ⦄ where → indexedSumᵐ f Preserves (_≡ᵉ_ on proj₁) ⟶ _≈_ indexedSumᵐ-cong {x = x , _ , h} {y , _ , h'} = indexedSum-cong {x = x , h} {y , h'} - module IndexedSumUnionᵐ (sp-∈ : spec-∈ A) (∈-A-dec : {X : Set A} → Decidable (_∈ X)) where + module IndexedSumUnionᵐ + (sp-∈ : spec-∈ A) (∈-A-dec : {X : Set A} → Decidable¹ (_∈ X)) where + open Unionᵐ sp-∈ ∪ᵐˡ-finite : {R R' : Rel A B} → finite R → finite R' → finite (R ∪ᵐˡ' R') diff --git a/src/Axiom/Set/TotalMap.agda b/src/Axiom/Set/TotalMap.agda index a9e32251d..acd5fdfa7 100644 --- a/src/Axiom/Set/TotalMap.agda +++ b/src/Axiom/Set/TotalMap.agda @@ -7,7 +7,6 @@ module Axiom.Set.TotalMap (th : Theory) where open import Prelude hiding (lookup) open import Agda.Primitive using () renaming (Set to Type) -open import Relation.Nullary.Decidable using (yes ; no) open import Function.Related.TypeIsomorphisms using (Σ-≡,≡→≡) open import Axiom.Set.Map th using (left-unique; Map ; mapWithKey-uniq ; left-unique-mapˢ) open import Axiom.Set.Rel th using (Rel ; dom ; dom∈) diff --git a/src/Axiom/Set/TotalMapOn.agda b/src/Axiom/Set/TotalMapOn.agda index 58ac4260a..1c198bcd0 100644 --- a/src/Axiom/Set/TotalMapOn.agda +++ b/src/Axiom/Set/TotalMapOn.agda @@ -10,7 +10,6 @@ open import Agda.Primitive using () renaming (Set to Type) open import Axiom.Set.Map th using (left-unique ; Map ; mapWithKey-uniq) open import Axiom.Set.Rel th using (Rel ; dom ; dom∈) open import Interface.DecEq using (DecEq ; _≟_) -open import Relation.Nullary.Decidable using (Dec ; yes ; no) open Theory th using ( Set ; _⊆_ ; _∈_ ; map ; ∈-map′ ) open Equivalence using (to) diff --git a/src/Ledger/Epoch.agda b/src/Ledger/Epoch.agda index a0b00bf36..22e8eaad2 100644 --- a/src/Ledger/Epoch.agda +++ b/src/Ledger/Epoch.agda @@ -23,52 +23,57 @@ record EpochStructure : Set₁ where StabilityWindow : Slot sucᵉ : Epoch → Epoch - _≥ˢ_ : Slot → Slot → Set - _≥ˢ_ = ¬_ ∘₂ _<ˢ_ + -- inequality - _≤ˢ_ : Slot → Slot → Set + _≥ˢ_ _≤ˢ_ : Slot → Slot → Set + _≥ˢ_ = ¬_ ∘₂ _<ˢ_ _≤ˢ_ = flip _≥ˢ_ + _<ᵉ_ _≤ᵉ_ : Epoch → Epoch → Set + _<ᵉ_ = _<ˢ_ on firstSlot + _≤ᵉ_ = _≤ˢ_ on firstSlot + open IsStrictTotalOrder Slot-STO using () renaming (_>=_; align; alignWith; ap; fromMaybe; map; zip; zipWith) public -open import Data.Unit hiding (_≟_) public -open import Data.Sum hiding (assocʳ; assocˡ; map; map₁; map₂; reduce; swap) public -open import Data.Product hiding (assocʳ; assocˡ; map; map₁; map₂; swap) public -open import Data.Nat hiding (_≟_; _≤_; _≤?_; _<_; __) public +open import Data.List public + hiding (align; alignWith; fromMaybe; map; zip; zipWith) +open import Data.List.Membership.Propositional public + using () renaming (_∈_ to _∈ˡ_) +open import Data.Maybe public + hiding (_>>=_; align; alignWith; ap; fromMaybe; map; zip; zipWith) public +open import Data.Unit public + hiding (_≟_) +open import Data.Sum public + hiding (assocʳ; assocˡ; map; map₁; map₂; reduce; swap) +open import Data.Product public + hiding (assocʳ; assocˡ; map; map₁; map₂; swap) +open import Data.Nat public + hiding (_≟_; _≤_; _≤?_; _<_; __) +open import Relation.Nullary public open import Relation.Nullary.Negation public -open import Relation.Binary.PropositionalEquality hiding (preorder; setoid; [_]; module ≡-Reasoning) public +open import Relation.Nullary.Decidable public + using (Dec; yes; no; dec-yes; dec-no; ⌊_⌋; ¬?; toWitness; fromWitness) +open import Relation.Unary public + using (Pred) renaming (Decidable to Decidable¹) +open import Relation.Binary public + using () renaming (Decidable to Decidable²) +open import Relation.Binary.PropositionalEquality public + hiding (preorder; setoid; [_]; module ≡-Reasoning) diff --git a/src/latex/agda-latex-macros.sty b/src/latex/agda-latex-macros.sty index d40cf4704..1490b2a11 100644 --- a/src/latex/agda-latex-macros.sty +++ b/src/latex/agda-latex-macros.sty @@ -251,9 +251,9 @@ \newcommand{\GovActionID}{\AgdaDatatype{GovActionID}\xspace} \newcommand{\GovActionIDFunction}{\AgdaFunction{GovActionID}\xspace} \newcommand{\GovActionState}{\AgdaRecord{GovActionState}\xspace} -\newcommand{\govDeposit}{\AgdaField{govDeposit}\xspace} +\newcommand{\govActionDeposit}{\AgdaField{govActionDeposit}\xspace} \newcommand{\GovernanceGroup}{\AgdaInductiveConstructor{GovernanceGroup}\xspace} -\newcommand{\govExpiration}{\AgdaField{govExpiration}\xspace} +\newcommand{\govActionLifetime}{\AgdaField{govActionLifetime}\xspace} \newcommand{\GovProposal}{\AgdaRecord{GovProposal}\xspace} \newcommand{\GovRole}{\AgdaDatatype{GovRole}\xspace} \newcommand{\GovVote}{\AgdaRecord{GovVote}\xspace} @@ -308,7 +308,7 @@ \newcommand{\maybeprime}{\AgdaFunction{maybe′}\xspace} \newcommand{\meetsMinAVS}{\AgdaFunction{meetsMinAVS}\xspace} \newcommand{\minimumAVS}{\AgdaField{minimumAVS}\xspace} -\newcommand{\minCCSize}{\AgdaField{minCCSize}\xspace} +\newcommand{\ccMinSize}{\AgdaField{ccMinSize}\xspace} \newcommand{\mleqmplusn}{\AgdaFunction{m≤m+n}\xspace} \newcommand{\module}{\AgdaKeyword{module}\xspace} \newcommand{\mostStakeDRepDist}{\AgdaFunction{mostStakeDRepDist}\xspace}