4 search results for "tag:"keyword: real numbers""

Showing 1 - 4
  1. coq-classical-realizability

    No documentation

    Krivine's classical realizability
    keyword: classical realizability keyword: Krivine's realizability keyword: primitive datatype keyword: non determinism keyword: quote keyword: axiom of countable choice keyword: real numbers category: Mathematics/Logic/Foundations
    Lionel Rieg <lionel.rieg@ens-lyon.org>
    8.10.0
    BSD
    Used by 0 other packages
    19 Oct 2020
  2. coq-coinductive-reals

    No documentation

    Real numbers as coinductive ternary streams
    keyword: real numbers keyword: co-inductive types keyword: co-recursion keyword: exact arithmetic category: Mathematics/Real Numbers date: 2007-04-24
    Milad Niqui <milad@cs.ru.nl> [http://www.cs.ru.nl/~milad]
    8.10.0
    LGPL
    Used by 0 other packages
    07 Dec 2019
  3. coq-exact-real-arithmetic

    No documentation

    Exact Real Arithmetic
    keyword: correctness keyword: real numbers keyword: arithmetic category: Mathematics/Real Numbers
    Jérôme Creci
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  4. coq-three-gap

    No documentation

    A Proof of the Three Gap Theorem (Steinhaus Conjecture)
    keyword: real numbers keyword: Steinhaus keyword: Three Gap Theorem category: Mathematics/Geometry category: Mathematics/Arithmetic and Number Theory/Miscellaneous
    Micaela Mayero
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019