From 09ccbf0adebac3f18a86e47293feed3c6ea876ec Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Sat, 5 Jul 2025 23:56:19 -0400 Subject: [PATCH] Wording tweak --- projects/Idris/src/TipsAndTricks/ProofSearchAndNonEquality.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/projects/Idris/src/TipsAndTricks/ProofSearchAndNonEquality.md b/projects/Idris/src/TipsAndTricks/ProofSearchAndNonEquality.md index 3619616..a484f77 100644 --- a/projects/Idris/src/TipsAndTricks/ProofSearchAndNonEquality.md +++ b/projects/Idris/src/TipsAndTricks/ProofSearchAndNonEquality.md @@ -11,7 +11,7 @@ import Decidable.Equality ## The Problem -When designing interfaces, you may occasionally find a need to thread a proof of non-equality through API, and for ergonomics reasons, you would like that proof to be an `auto` implicit so the user doesn't have to generate the proof manually. Often, these proofs seem like they really should be trivial for the compiler to generate. +When designing interfaces, you may occasionally find a need to thread a proof of non-equality through API, and for ergonomics reasons, you would like that proof to be an `auto` implicit so the user doesn't have to generate the proof manually. Often, these proofs seem like they really should be trivial for the compiler to generate, but proof search will adamantly refuse to do so. I recently came across an instance of this implementing the _Brown Benchmark for Table Types_[^1], where I needed to encode a proof that a given value was non-equal to every value currently in a list (much like a _FreshList_[^2], but with propositional equality). In many cases, this list is going to be know statically at compile time, so I would like the compiler to just generate the structure when possible to keep the API easy to use.