thatonelutenist/website
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Wording tweak

Browse source
This commit is contained in:
Nathan McCarty 2025-07-05 23:56:19 -04:00
parent 83a98e6237
commit 09ccbf0ade
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
projects/Idris/src/TipsAndTricks/ProofSearchAndNonEquality.md
View file

@ -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.