From fd2c04049065b4a995424286ea98e019f142c20a Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 1 Aug 2025 07:46:15 +0100 Subject: [PATCH 1/4] add: recommendation --- doc/style-guide.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/doc/style-guide.md b/doc/style-guide.md index 7da14eb7f5..e1c7e5271d 100644 --- a/doc/style-guide.md +++ b/doc/style-guide.md @@ -717,3 +717,7 @@ used successfully in PR systematic for `Nary` relations in PR [#811](https://github.com/agda/agda-stdlib/pull/811) +## Prefer use of `Relation.Nullary.Negation.Core.contradiction` + +Where possible, `contradiction`, as a higher-level encapsulated abstraction, +is to be preferred over direct appeal to `Data.Empty.⊥-elim`. \ No newline at end of file From 08b8d7583438ab20a35453dab053fd1e5fbc9887 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 1 Aug 2025 07:50:36 +0100 Subject: [PATCH 2/4] fix: whitespace --- doc/style-guide.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/style-guide.md b/doc/style-guide.md index e1c7e5271d..059c21c899 100644 --- a/doc/style-guide.md +++ b/doc/style-guide.md @@ -720,4 +720,4 @@ systematic for `Nary` relations in PR ## Prefer use of `Relation.Nullary.Negation.Core.contradiction` Where possible, `contradiction`, as a higher-level encapsulated abstraction, -is to be preferred over direct appeal to `Data.Empty.⊥-elim`. \ No newline at end of file +is to be preferred over direct appeal to `Data.Empty.⊥-elim`. From a45010426045fabe5ce07ad61067769766f2bbd9 Mon Sep 17 00:00:00 2001 From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Date: Sat, 2 Aug 2025 09:39:45 +0100 Subject: [PATCH 3/4] Update doc/style-guide.md Improved text. Co-authored-by: Jacques Carette --- doc/style-guide.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/style-guide.md b/doc/style-guide.md index 059c21c899..b6f504a32f 100644 --- a/doc/style-guide.md +++ b/doc/style-guide.md @@ -719,5 +719,5 @@ systematic for `Nary` relations in PR ## Prefer use of `Relation.Nullary.Negation.Core.contradiction` -Where possible, `contradiction`, as a higher-level encapsulated abstraction, -is to be preferred over direct appeal to `Data.Empty.⊥-elim`. +Where possible use `contradiction` between two explicit arguments rather than appealing to the lower-level +`Data.Empty.⊥-elim`. This provides clearer documentation for readers of the code. From d206dfa4e50e7edbb2a8858ff664bdef650c3e5a Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 2 Aug 2025 11:25:28 +0100 Subject: [PATCH 4/4] fix: `fill-column` to 72 --- doc/style-guide.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/doc/style-guide.md b/doc/style-guide.md index b6f504a32f..cfecfbd699 100644 --- a/doc/style-guide.md +++ b/doc/style-guide.md @@ -719,5 +719,6 @@ systematic for `Nary` relations in PR ## Prefer use of `Relation.Nullary.Negation.Core.contradiction` -Where possible use `contradiction` between two explicit arguments rather than appealing to the lower-level -`Data.Empty.⊥-elim`. This provides clearer documentation for readers of the code. +Where possible use `contradiction` between two explicit arguments rather +than appealing to the lower-level `Data.Empty.⊥-elim`. This provides +clearer documentation for readers of the code.