• Guillaume Melquiond's avatar
    Started a realization of real.real. · 72b12557
    Guillaume Melquiond authored
    This is just a proof of concept, since most definitions should just be
    notations for the realization to be user-friendly. Moreover, the format of
    the file will presumably evolve, if only for some information to properly
    update it when the theories change.
    
    Remark about the theory : Lemma mul_assoc_div has an extraneous hypothesis.
    Indeed, as long as inverse is a total function, this lemma is an immediate
    consequence of multiplication associativity.
    72b12557
Name
Last commit
Last update
bench Loading commit data...
bin Loading commit data...
comparison Loading commit data...
doc Loading commit data...
drivers Loading commit data...
examples Loading commit data...
misc Loading commit data...
modules Loading commit data...
plugins Loading commit data...
realizations/coq/real Loading commit data...
share Loading commit data...
src Loading commit data...
tests Loading commit data...
theories Loading commit data...
.gitignore Loading commit data...
CHANGES Loading commit data...
DEVELOPER.readme Loading commit data...
INSTALL Loading commit data...
LICENSE Loading commit data...
META.in Loading commit data...
Makefile.in Loading commit data...
OCAML-LICENSE Loading commit data...
README Loading commit data...
ROADMAP Loading commit data...
TODO Loading commit data...
Version Loading commit data...
configure.in Loading commit data...