agda-stdlib (not 2.0); ring solver sanity check

conal · Feb 12, 2024 · dc45407 · dc45407
1 parent b3208da
commit dc45407
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 1 deletion.
diff --git a/felix.agda-lib b/felix.agda-lib
@@ -1,3 +1,3 @@
 name: felix
-depend: standard-library-2.0
+depend: standard-library
 include: src
diff --git a/src/Felix/All.agda b/src/Felix/All.agda
@@ -2,6 +2,10 @@
 
 module Felix.All where
 
+-- Temporary sanity check while finding a commit point in agda-stdlib that will
+-- work with agda-2.6.3 and Felix and reflection (particularly the ring solver).
+open import Data.Nat.Tactic.RingSolver using (solve-∀)
+
 import Felix.Object
 import Felix.Equiv
 import Felix.Raw