package coq-mathcomp-bigenough

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

Install

Dune Dependency

github.com Edit opam file Versions (2)

Authors

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

Maintainers

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

Sources

1.0.0.tar.gz
md5=cf126ccb8a405eb2e94f68d57152b717

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

Published: 08 Aug 2018

Dependencies (3)

  1. coq-mathcomp-ssreflect >= "1.6"
  2. coq >= "8.5" & < "8.15~"
  3. ocaml

Dev Dependencies

None

Conflicts

None