From dc454074c3f6747147ddd5262549073bf555cfda Mon Sep 17 00:00:00 2001 From: Conal Elliott Date: Sun, 11 Feb 2024 19:58:27 -0800 Subject: [PATCH] agda-stdlib (not 2.0); ring solver sanity check --- felix.agda-lib | 2 +- src/Felix/All.agda | 4 ++++ 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/felix.agda-lib b/felix.agda-lib index cef6dab..4d6935e 100644 --- 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 index 8837fe1..b8300a1 100644 --- 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