update agda-stdlib

Coords.agda

@@ -1,9 +1,9 @@
 open import Data.Nat
 open import Data.Integer using (∣_∣; _⊖_)
 open import Data.Product
-open import Data.Fin
+open import Data.Fin hiding (_≟_)
 open import Relation.Binary using (Decidable)
-open import Relation.Binary.PropositionalEquality renaming (proof-irrelevance to ≡-irrelevance)
+open import Relation.Binary.PropositionalEquality
 
 open import Enumeration as Enum using (Enumeration)
 

Enumeration.agda

@@ -1,10 +1,12 @@
 module Enumeration where
 
 open import Data.List as List using (List; []; _∷_)
+import Data.List.Categorical as List
 open import Data.List.Any
 import Data.List.Any.Properties as AnyProp
-open import Data.List.Any.Membership.Propositional
-import Data.List.Any.Membership.Propositional.Properties as ∈Prop
+open import Data.List.Membership.Propositional
+import Data.List.Membership.Propositional.Properties as ∈Prop
+open import Data.List.Relation.BagAndSetEquality
 open import Data.Fin
 import Data.Fin.Properties as FinProp
 open import Data.Nat as ℕ
@@ -206,21 +208,13 @@ enum₁ ⊗ enum₂ = record
 
 
 private
-  -- for until the next release, when it's in Relation.Binary.PropositionalEquality
-  isPropositional : ∀ {a} → Set a → Set a
-  isPropositional A = (a b : A) → a ≡ b
-
-  IrrelevantPred : ∀ {a ℓ} {A : Set a} → (A → Set ℓ) → Set (ℓ Level.⊔ a)
-  IrrelevantPred P = ∀ {x} → isPropositional (P x)
-
   module Filter {A : Set} {P : A → Set} (P-irrelevant : IrrelevantPred P) (P? : Decidable P) where
     discardNo : ∀ {a} → Dec (P a) → Maybe (Σ A P)
     discardNo {a = a} (yes p) = just (a , p)
     discardNo (no ¬p) = nothing
 
-    -- also change gfilter to mapMaybe
     Σfilter : List A → List (Σ A P)
-    Σfilter = List.gfilter (discardNo ∘ P?)
+    Σfilter = List.mapMaybe (discardNo ∘ P?)
 
     Σfilter-∈ : ∀ {xs x} → x ∈ xs → (Px : P x) → (x , Px) ∈ Σfilter xs
     Σfilter-∈ {x ∷ xs} (here refl) Px with P? x

Rules.agda

@@ -3,8 +3,8 @@
 open import Data.Unit
 open import Data.Product
 open import Data.Nat as ℕ using (ℕ)
-open import Data.List
-open import Relation.Binary.PropositionalEquality renaming (proof-irrelevance to ≡-irrelevance)
+open import Data.List hiding (lookup)
+open import Relation.Binary.PropositionalEquality
 open import Relation.Binary using () renaming (Decidable to Decidable₂)
 open import Relation.Unary  using () renaming (Decidable to Decidable₁)
 open import Relation.Nullary
@@ -23,7 +23,7 @@ _[_]✓ {bounds} grid coords with lookup coords grid
 ... | safe n = Σ[ neighboringMines ∈ Enumeration (mine Neighboring coords on grid) ] n ≡ length (Enumeration.list neighboringMines)
 
 _✓ : ∀ {bounds} → Board KnownTile bounds → Set
-_✓ {bounds} grid = ∀ coords -> grid [ coords ]✓
+_✓ {bounds} grid = ∀ coords → grid [ coords ]✓
 
 mine? : Decidable₁ (_≡_ mine)
 mine? mine     = yes refl

minesweeper-reasoning.agda-lib

@@ -0,0 +1,3 @@
+name: minesweeper-reasoning
+depend: standard-library
+include: .