-
Notifications
You must be signed in to change notification settings - Fork 8
/
meta.yml
97 lines (83 loc) · 2.34 KB
/
meta.yml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
---
fullname: Mczify
shortname: mczify
opam_name: coq-mathcomp-zify
organization: math-comp
action: true
synopsis: >-
Micromega tactics for Mathematical Components
description: |-
This small library enables the use of the Micromega arithmetic solvers of Coq
for goals stated with the definitions of the Mathematical Components library
by extending the zify tactic.
authors:
- name: Kazuhiko Sakaguchi
initial: true
opam-file-maintainer: [email protected]
license:
fullname: CeCILL-B Free Software License Agreement
identifier: CECILL-B
file: CeCILL-B
supported_coq_versions:
text: 8.16 or later
opam: '{>= "8.16"}'
tested_coq_nix_versions:
tested_coq_opam_versions:
- version: '2.0.0-coq-8.16'
repo: 'mathcomp/mathcomp'
- version: '2.0.0-coq-8.17'
repo: 'mathcomp/mathcomp'
- version: '2.0.0-coq-8.18'
repo: 'mathcomp/mathcomp'
- version: '2.1.0-coq-8.16'
repo: 'mathcomp/mathcomp'
- version: '2.1.0-coq-8.17'
repo: 'mathcomp/mathcomp'
- version: '2.1.0-coq-8.18'
repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-8.16'
repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-8.17'
repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-8.18'
repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-8.19'
repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-8.20'
repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-dev'
repo: 'mathcomp/mathcomp'
- version: 'coq-8.18'
repo: 'mathcomp/mathcomp-dev'
- version: 'coq-8.19'
repo: 'mathcomp/mathcomp-dev'
- version: 'coq-8.20'
repo: 'mathcomp/mathcomp-dev'
- version: 'coq-dev'
repo: 'mathcomp/mathcomp-dev'
dependencies:
- opam:
name: coq-mathcomp-ssreflect
version: '{>= "2.0"}'
description: |-
[MathComp](https://math-comp.github.io) ssreflect 2.0 or later
- opam:
name: coq-mathcomp-algebra
description: |-
[MathComp](https://math-comp.github.io) algebra
test_target: test-suite
namespace: mathcomp.zify
action_appendix: |2-
export: 'OPAMWITHTEST'
env:
OPAMWITHTEST: true
documentation: |-
## File contents
- `zify_ssreflect.v`: Z-ification instances for the `coq-mathcomp-ssreflect`
library
- `zify_algebra.v`: Z-ification instances for the `coq-mathcomp-algebra`
library
- `zify.v`: re-exports all the Z-ification instances
- `ssrZ.v`: provides a minimal facility for reasoning about `Z` and relating
`Z` and `int`
---