feat: document the function application naming convention#886
feat: document the function application naming convention#886YaelDillies wants to merge 4 commits into
Conversation
b-mehta
left a comment
b-mehta
left a comment
There was a problem hiding this comment.
I agree with the spirit of this convention, but I think the current phrasing is not very clear.
| 3. The application is denoted by the `map_` prefix when `f` is a free variable | ||
| or the coercion to function thereof, and `x` is a concrete argument. | ||
| Most lemmas of this form are about properties of a generic morphism. | ||
|
|
There was a problem hiding this comment.
Your change is an improvement, but I think it's still a little ambiguous whether or not a + b is concrete or not... I wonder if it's easier to explain in terms of what's named. In all your examples, concrete and "is part of the name" coincide exactly
There was a problem hiding this comment.
Hmm, I am not sure. Beginners sometimes name their lemmas after free variables, no?
There was a problem hiding this comment.
Fair point, but I still think your phrasing doesn't sufficiently explain what happens to a + b
There was a problem hiding this comment.
I've attempted something. I personally find it more confusing now, but you might disagree
There was a problem hiding this comment.
Also note that I show below * as an example of a concrete function, so maybe there was no need to clarify in the first place?
There was a problem hiding this comment.
Actually that was the reason it confused me, from your description I didn't think you intended it to be a concrete function, but your example included it.
There was a problem hiding this comment.
Aha ok 😆 I hope now the phrasing is clear enough?
3 participants
No description provided.