From bb082778ca2807a9af0af1e666e0f6a9fd73cab1 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Thu, 18 Jun 2026 06:41:46 +0200 Subject: [PATCH 1/2] Make final parameter of Acc an index --- src/Induction/WellFounded.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Induction/WellFounded.agda b/src/Induction/WellFounded.agda index 4d5aec6a74..f84ff2c098 100644 --- a/src/Induction/WellFounded.agda +++ b/src/Induction/WellFounded.agda @@ -43,8 +43,8 @@ WfRec _<_ P x = ∀ {y} → y < x → P y -- The accessibility predicate: x is accessible if everything which is -- smaller than x is also accessible (inductively). -data Acc {A : Set a} (_<_ : Rel A ℓ) (x : A) : Set (a ⊔ ℓ) where - acc : (rs : WfRec _<_ (Acc _<_) x) → Acc _<_ x +data Acc {A : Set a} (_<_ : Rel A ℓ) : (x : A) → Set (a ⊔ ℓ) where + acc : ∀ {x} (rs : WfRec _<_ (Acc _<_) x) → Acc _<_ x -- The accessibility predicate encodes what it means to be -- well-founded; if all elements are accessible, then _<_ is From 8a0f1744ed60b0ba495ab027524ad816d06f371b Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Thu, 18 Jun 2026 06:45:35 +0200 Subject: [PATCH 2/2] Changelog --- CHANGELOG.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 3867278c6c..80fe780134 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -42,6 +42,9 @@ Non-backwards compatible changes Minor improvements ------------------ +* In `Induction.WellFoudned`, the final parameter of `Acc` has been changed to + an index. + Deprecated modules ------------------