mf: a coq library for multivalued functions. The only dependency is ssreflect. It was tested with version 1.7. and Coq version 8.9.0.

To install copy and paste to any folder (best just clone the repository), then run "make" and then "make install" and you're all set.

There are parts that use classical reasoning and choice principles. These parts are not exported by the all_mf file but have to be imported separately.