diff options
| author | Hugo Herbelin | 2016-10-02 21:48:52 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-03-03 14:40:36 +0100 |
| commit | 62ed11de4c528a496e0ece70a07062a1b6d4f7d8 (patch) | |
| tree | 8c32a1e71bfc7e3d3ff27029f2c5588b141f72fa /kernel/nativecode.mli | |
| parent | b453d0281db6de0c36cbd9f2c0a094946f4fcfd6 (diff) | |
Adding various properties and characterization of the extensional
axiom of choice (i.e. choice on setoids) and of the axiom selecting
representatives in classes of equivalence.
Also integrating suggestions from Théo.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions