meta.yml

---
fullname: bigenough
shortname: bigenough
opam_name: coq-mathcomp-bigenough
organization: math-comp
community: false
action: true
coqdoc: false
dune: false

synopsis: >-
  A small library to do epsilon - N reasoning

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.

authors:
- name: Cyril Cohen

maintainers:
- name: Cyril Cohen
  nickname: CohenCyril

opam-file-maintainer: 'Cyril Cohen <cyril.cohen@inria.fr>'

opam-file-version: 'dev'

license:
  fullname: CeCILL-B
  identifier: CeCILL-B

supported_coq_versions:
  text: '8.10 or later'
  opam: '{(>= "8.10" & < "8.15~") | (= "dev")}'

dependencies:
- opam:
    name: coq-mathcomp-ssreflect
    version: '{>= "1.6"}'
  description: |-
    [MathComp ssreflect](https://math-comp.github.io) 1.6 or later

tested_coq_opam_versions:
- version: '8.10'
- version: '8.11'
- version: '8.12'
- version: '8.13'
- version: '8.14'
- version: 'dev'

namespace: mathcomp.bigenough

keywords:
- name: bigenough
- name: asymptotic reasonning
- name: small scale reflection
- name: mathematical components

documentation: |-
  # A small library to do epsilon - N reasoning.

  This repository is essentially for archiving purposes as `bigenough`
  will be subsumed by the [near tactics](https://github.com/math-comp/analysis/blob/9bfd5a1971c6989f51d9c44341bb71b2fd5e3c76/topology.v#L93).

  The formalization is based on the [Mathematical Components](https://github.com/math-comp/math-comp) library for the [Coq](https://coq.inria.fr) proof assistant,
  although it requires only the ssreflect package.
---