Fix #6066: document redundant pattern directives in records

agda · Oct 5, 2022 · 1097d0a · 1097d0a
1 parent 53143b4
commit 1097d0a
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/doc/user-manual/language/record-types.lagda.rst b/doc/user-manual/language/record-types.lagda.rst
@@ -459,6 +459,12 @@ is on.  If you want the converse, you can add the record directive
   pred : HereditaryList → List HereditaryList
   pred record{ sublists = ts } = ts
 
+If both ``eta-equality`` and ``pattern`` are given for a record types,
+Agda will alert the user of a redundant ``pattern`` directive.
+However, if η is inferred but not declared explicitly, Agda will just
+ignore a redundant ``pattern`` directive; this is because the default
+can be changed globally by option :option:`--no-eta-equality`.
+
 .. _instance-fields:
 
 Instance fields