package coq-qarith-stern-brocot

  1. Overview
  2. No Docs
Binary rational numbers in Coq

Install

Dune Dependency

github.com Edit opam file Versions (10)

Authors

  1. M
    Milad Niqui
  2. Y
    Yves Bertot

Maintainers

  1. P
    palmskog@gmail.com

Sources

v8.14.0.tar.gz
sha512=bc553ba930da80608c87c968016b7b8733a806aa65c510cc9834aca4933710ac21173d3691837bf09c3aba34849f320442086bf05081e22121fef97b084611b4

Description

Development of rational numbers in Coq as finite binary lists and defining field operations on them in two different ways: strict and lazy.

Tags

category:Mathematics/Arithmetic and Number Theory/Rational numbers category:Miscellaneous/Extracted Programs/Arithmetic keyword:rational numbers keyword:arithmetic keyword:field tactic keyword:binary lists keyword:Stern-Brocot logpath:QArithSternBrocot date:2021-10-30

Published: 30 Oct 2021

Dependencies (1)

  1. coq >= "8.14" & < "8.18~"

Dev Dependencies

None

Used by

None

Conflicts

None