diff options
| author | Hugo Herbelin | 2016-10-12 18:58:41 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-03-03 14:44:42 +0100 |
| commit | 620f1918452b898d6663cabb5e0f341c7e767017 (patch) | |
| tree | 5618a6e05035f0b6fc03c8f8c3104140aba61b78 /kernel/type_errors.mli | |
| parent | 4e85cc6e9792da116f1b20e484b2ce629c6f6865 (diff) | |
Strengthening some of the results in ChoiceFacts.v.
Further highlighting when the correspondence between variants of
choice is independent of the domain and codomain of the function, as
was done already done in the beginning of the file (suggestion from
Jason).
Adding some corollaries.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions