Switch branches/tags
Nothing to show
Commits on Dec 14, 2010
  1. removing comments

    committed Dec 14, 2010
  2. Fitting into 30pp

    committed Dec 14, 2010
  3. Revert "Adding references."

    This reverts commit 1174104.
    committed Dec 14, 2010
Commits on Dec 13, 2010
  1. Adding references.

    committed Dec 13, 2010
  2. Minor MSCS paper polishing.

    Eelis committed Dec 13, 2010
Commits on Dec 10, 2010
  1. Partially reinstate cons_list.

    Eelis committed Dec 10, 2010
  2. Add references to MSCS paper.

    Eelis committed Dec 10, 2010
Commits on Dec 9, 2010
Commits on Dec 8, 2010
Commits on Dec 7, 2010
  1. Implemented the bit shift operations on ZType_integers using Pierre's…

    … new implementations in Zsig. Introduced the notion of notion of order preserving maps. Cancellation on rings revised.
    robbertkrebbers committed Dec 7, 2010
Commits on Dec 2, 2010
  1. Merge Robbert's work.

    Eelis committed Dec 2, 2010
  2. Replace default equality on function types with ((=)==>(=)). Add Seto…

    …id-specialized Functor type class. Add do-notation for monads. Add some theory for functors and monads.
    Eelis committed Dec 2, 2010
Commits on Dec 1, 2010
  1. .gitignore *.pyc.

    Eelis committed Dec 1, 2010
  2. Expand implementations/ne_list.

    Eelis committed Dec 1, 2010
  3. Parameterize coqc executable name in Coq SCons builder (so that it ca…

    …n be set to ssrcoq easily).
    Eelis committed Dec 1, 2010
Commits on Nov 26, 2010
  1. Embedding of the dyadics into Q finished.

    * Approximate operations on the dyadics
    * Eelis' hack to fix slow [decide (x = y)] on ZType integers
    * Induction principles for the integers
    * Some new benchmarks
    * theory.cut_minus cleaned up
    * Some additional properties of fields
    robbertkrebbers committed Nov 26, 2010
Commits on Nov 25, 2010
  1. Forgot theory.rationals

    robbertkrebbers committed Nov 25, 2010
  2. Fix typo.

    Eelis committed Nov 25, 2010
  3. Merge Robbert's work.

    Eelis committed Nov 25, 2010
Commits on Nov 23, 2010
Commits on Nov 20, 2010
  1. Merge branch 'master' of git://

    robbertkrebbers committed Nov 20, 2010
Commits on Nov 19, 2010
  1. Many changes, most importantly, maps between the dyadics and rationals.

    * Implicit parameters of stdlib_{ring,field,semiring}_theory fixed.
    * Ad hoc hack to make fast_integers use BigN's shiftl and shiftr.
    * Moved theory about rationals from interfaces.rationals to theory.rationals.
    * A structure isomorphic to some rationals is also a rationals.
    * The above made it possible to cleanup implementations.QType_rationals nicely.
    * An embedding of fast_integers into fast_rationals. This allows for an
      embedding of the dyadics build from the fast_integers into the fast_rationals
      with which we can actually compute.
    * A map to go back from the fast_rationals to the fast_integers. As a result, I
      have written an approximate embedding of the rationals in the dyadics.
    * Moved theory.MinMax to orders.minmax and basically reorganized the file. Also
      dyadics now uses orders.minmax instead of his own min function.
    * I am now using a dollar sign instead of a dash to denote dyadics so as to
      avoid conflicts with the notation for rationals.
    * Attempted to generalize the specification of nat_pow to int_pow. Although
      theory about this is not present yet.
    * Some new results about arbitrary rings and fields.
    * Many dirty names cleaned up.
    * New tests involving computation with dyadics.
    robbertkrebbers committed Nov 19, 2010