Update Agda to 2.7 (#1257)

IntersectMBO · Sep 20, 2024 · 3b1b756 · 3b1b756
2 parents a2de31b + e91c4e1
commit 3b1b756
Show file tree

Hide file tree

Showing 4 changed files with 9 additions and 69 deletions.
diff --git a/docs/agda-spec/src/Interface/HasOrder/Instance.agda b/docs/agda-spec/src/Interface/HasOrder/Instance.agda
@@ -26,10 +26,6 @@ instance
 
   open import Data.Rational using (ℚ)
   import Data.Rational.Properties as Rat hiding (_≟_)
-
-  ℚ-Dec-≤ = ⁇² Rat._≤?_
-  ℚ-Dec-< = ⁇² Rat._<?_
-
   ℚ-hasPreorder = hasPreorderFromNonStrict Rat.≤-isPreorder _≟_
   ℚ-hasPartialOrder = HasPartialOrder ∋ record { ≤-antisym = Rat.≤-antisym }
   ℚ-hasDecPartialOrder = HasDecPartialOrder {A = ℚ} ∋ record {}
diff --git a/docs/agda-spec/src/Tactic/ByEq.agda b/docs/agda-spec/src/Tactic/ByEq.agda
diff --git a/flake.lock b/flake.lock
diff --git a/nix/agda.nix b/nix/agda.nix
@@ -21,10 +21,10 @@ let
     pname = "agda-stdlib-classes";
     version = "2.0";
     src = pkgs.fetchFromGitHub {
-      repo = "agda-stdlib-classes";
       owner = "omelkonian";
+      repo = "agda-stdlib-classes";
       rev = "v2.0";
-      sha256 = "4ujdQv38u6BybFhRup9PMR0xpI59J/Naz/kaBtQQ9aY=";
+      hash = "sha256-PcieRRnctjCzFCi+gUYAgyIAicMOAZPl8Sw35fZdt0E=";
     };
     meta = { };
     libraryFile = "agda-stdlib-classes.agda-lib";
@@ -37,10 +37,10 @@ let
     pname = "agda-stdlib-meta";
     version = "2.0";
     src = pkgs.fetchFromGitHub {
-      repo = "stdlib-meta";
-      owner = "input-output-hk";
-      rev = "4fc4b1ed6e47d180516917d04be87cbacbf7d314";
-      sha256 = "T+9vwccbDO1IGBcGLjgV/fOt+IN14KEV9ct/J6nQCsM=";
+      owner = "omelkonian";
+      repo = "agda-stdlib-meta";
+      rev = "v2.1.1";
+      hash = "sha256-qOoThYMG0dzjKvwmzzVZmGcerfb++MApbaGRzLEq3/4=";
     };
     meta = { };
     libraryFile = "agda-stdlib-meta.agda-lib";