Make the property argument to replace explicit
#3531
Conversation
| In practice, this function can be a little tricky to use because in | ||
| general the argument ``p`` can be hard to infer by unification, so | ||
| Idris provides a high level syntax which calculates the property | ||
| and applies ``replace``: |
There was a problem hiding this comment.
I don't quite follow the logic here, but I've kept it as similar as possible in wording. Do edit it if you know a better wording (also in the other file which duplicates this)
There was a problem hiding this comment.
I don't think there is any "infer by unification" here anymore, since p was implicit and this PR makes it explicit. Maybe something along the lines of "the argument p is cumbersome to write, so Idris provides ....".
In practice, I use replace when Idris can't figure out p in rewrite, especially in the case where I only want to replace a subset of the occurrences of a term. But others who have more experience with using Idris for proofs than I do. I've always had to specify p when I use replace.
| @@ -2,6 +2,6 @@ import Data.Vect | |||
| record Foo (th : Vect n a) where | |||
| nIsZero : n === 0 | |||
| vectIsEmpty : (th ===) | |||
| $ replace {p = \ n => Vect n a} (sym nIsZero) | |||
| $ replace (\ n => Vect n a) (sym nIsZero) | |||
There was a problem hiding this comment.
not sure if I've broken this test, or what it tests
There was a problem hiding this comment.
deleting this test is likely not the correct action, but I'm unclear what it's testing so waiting for someone to enlighten me
There was a problem hiding this comment.
perhaps that a space is expected in {p=\n ...
There was a problem hiding this comment.
The original commit is #2781 (git has a hard time telling you because the files were moved around). Maybe we could find an example that doesn't use replace. Similar issue, I think it was no space after the =, but the error message itself should point to the correct location rather than saying "couldn't parse declaration". Any implicit pattern match that fails because of a missing space would do. (The "perror" tests are for parse errors.)
Description
replacecan almost never infer the propertyp, so I've made it explicit, after @gallais ' agreementShould this change go in the CHANGELOG?
implementation, I have updated
CHANGELOG_NEXT.md(and potentially alsoCONTRIBUTORS.md).