diff options
| author | Gaetan Gilbert | 2017-05-02 14:43:32 +0200 |
|---|---|---|
| committer | Gaetan Gilbert | 2017-05-03 13:39:51 +0200 |
| commit | 8adfa0e5290056b7683a3a8b778ca16182a1eb3d (patch) | |
| tree | 513edd44778a8c5c321b0004829d1458bbac527d /dev/include | |
| parent | fdd5a8452bd2da22ffd1cab3b1888f2261f193b9 (diff) | |
Reorganize comment documentation of ChoiceFacts.v
Shortnames and natural language descriptions of principles are moved
next to each principle.
The table of contents is moved to after the principle definitions.
Extra definitions are moved to the definition section (eg DependentFunctionalChoice)
Compatibility notations have been moved to the end of the file.
Details:
The following used to be announced but were neither defined or used,
and have been removed:
- OAC!
- Ext_pred = extensionality of predicates
- Ext_fun_prop_repr = choice of a representative among extensional functions to Prop
GuardedFunctionalRelReification was announced with shortname GAC! but
shortname GFR_fun was used next to it. Only the former has been retained.
Shortnames and descriptions have been invented for
InhabitedForallCommute DependentFunctionalRelReification
ExtensionalPropositionRepresentative ExtensionalFunctionRepresentative
Some modification of headlines
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions