aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/stdlib
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-10-02 21:48:52 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-03-03 14:40:36 +0100
commit62ed11de4c528a496e0ece70a07062a1b6d4f7d8 (patch)
tree8c32a1e71bfc7e3d3ff27029f2c5588b141f72fa /doc/stdlib
parentb453d0281db6de0c36cbd9f2c0a094946f4fcfd6 (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 'doc/stdlib')
0 files changed, 0 insertions, 0 deletions