From 9ce70eab7288cdac762cf9b6243a19521fa6485e Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Wed, 24 Sep 2025 18:06:40 +1000
Subject: [PATCH] feat(style): avoid nonrec

---
 templates/contribute/style.md | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/templates/contribute/style.md b/templates/contribute/style.md
index 4ed3d57c7..9f227b17c 100644
--- a/templates/contribute/style.md
+++ b/templates/contribute/style.md
@@ -638,3 +638,10 @@ We allow, but discourage, contributors from simultaneously renaming declarations
 In this case, no deprecation attribute is required for X, but it is for W.
 
 Named instances do not require deprecations. Deprecated declarations can be deleted after 6 months.
+
+### Avoid `nonrec`
+
+The `nonrec` keyword tells Lean to assume that apparently recursive calls in the declaration body
+are not actually recursive, and instead look for declarations in other namespaces with the same name.
+It is nearly always clearer to disambiguate the call by using an explicit namespace,
+and this should be preferred where possible. (There are currently many places in Mathlib that break this rule.)