Type of suggested lemma in Bin-isomorphism compiles #1083
Conversation
negatratoron
force-pushed
the
fix-bin-isomorphism-exercise-type
branch
from
df32db1 to
345b7d6
Compare
|
Ahh, I think the problem is the Sigma record was not opened. I was a little surprised Agda didn't figure out that proj_1 referred to the Sigma field, turns out that's because it wasn't in scope. |
There was a problem hiding this comment.
Well spotted. I'm always forgetting to open records. Thanks for that save!
I think it's important also to remove the import of Data.Product, else there will be a clash of names. Can you do that as well?
And with the import removed, the definition of \times' can lose the prime (and the sentence drawing attention to the prime). Could you please make this fix as well?
Thank you for your help!
That definition is used in the Universals exercises, so I don't think it can just be deleted. The definition has to exist for those exercises to compile. You're welcome :) |
|
Re-requesting a review. I don't think the Data.Product import could be removed (other than by re-defining products or importing the earlier Connectives chapter) without significantly affecting the Universals exercises (somehow removing product from them, or moving them below the product definition in the Existentials section). |
There was a problem hiding this comment.
Elsewhere in the chapter, \times is defined. (Once you remove the prime, as I requested previously.) And it is defined in terms of \Sigma, so has proj_1 and proj_2 defined. So the exercises will be fine, they just use the product defined in the chapter, which is defined in exactly the same way as in Data.Product.
More generally, there is a tension between using the operations as defined in the chapters and using the operations from the Standard Library. In Lean, documentation is sometimes written with a separate, hidden set of imports for each code block. That has the advantage of being able to define product in one code block and then use the one imported from the standard library in the next code block. But it has the disadvantage that if you read the book without opening each block you don't know what imports are in scope.
|
Maybe I don't understand what you're saying, but if I make this change: negatratoron@472f8bb I get an error "Not in scope: \times" from the exercise on line 94. From the Agda docs:
Separating the signature from the definition is possible, but these exercises depend on the definition of \times, so it's not enough to just declare "\times : Set \to Set \to Set", it has to have its full definition present. The key thing is, \times is used in exercises before products are defined in terms of Sigma. |
Fixes #1003
The type signature compiles by qualifying the function "proj_1". Also added a sentence calling this out.