Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I added to decidable equality some remarks on the difference between the propositions-as-types version and the propositions-as-some-types version.
Nice!
Over here somebody shows that he found the paragraph at decidable equality on Applications confusing.
I suppose the paragraph was okay in itself and no expert would have found it confusing, but I see how for a novice it may not have been clear enough that throughout the entry the word “set” means different things depending on whether it is understood that one speaks constructively or not.
In any case, I have edited ever so slightly in an attempt to clarify. But please feel invited to edit further.
1 to 6 of 6