Typo in Polymorphism.v
Closed this issue · 3 comments
bkushigian commented
In lines 18-22 of Polymorphism.v there is a typo describing option
. I'd do a PR but I'm not quite sure what it should say:
While Java and friends force all sorts of different types to include the special value [null],
in Coq we request that option explicitly [something here] by wrapping a type in [option].
p0llard commented
I don't think this is a typo; if you replace 'that' with 'this' it might be easier to parse. The first occurrence of the word option is using it in its normal, dictionary definition sense.
achlipala commented
This could be a corner case of the way I perceive English, but the original sounds fine to me. The word "explicitly" is an adverb modifying "request."
bkushigian commented
No no, you're right, this was a parse error on my part