package coq-mathcomp-bigenough

  1. Overview
  2. No Docs
A small library to do epsilon - N reasoning

Install

Dune Dependency

github.com Edit opam file Versions (2)

Authors

  1. C
    Cyril Cohen

Maintainers

  1. C
    Cyril Cohen <cyril.cohen@inria.fr>

Sources

1.0.1.tar.gz
sha256=a8ed105271ca7422f87f580ba1c5bb39de9f147ad966e65e02d09010cb3c1e36

Description

The package contains a package to reasoning with big enough objects (mostly natural numbers). This package is essentially for backward compatibility purposes as bigenough will be subsumed by the near tactics. The formalization is based on the Mathematical Components library.

Tags

keyword:bigenough keyword:asymptotic reasonning keyword:small scale reflection keyword:mathematical components logpath:mathcomp.bigenough

Published: 10 Dec 2021

Dependencies (1)

  1. coq-mathcomp-ssreflect >= "1.6"

Dev Dependencies (1)

  1. coq (>= "8.10" & < "8.21~") | (= "dev")

Conflicts

None