-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathmeta.yml
132 lines (91 loc) · 3.24 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
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
---
fullname: mathcomp-extra
shortname: mathcomp-extra
organization: thery
community: false
dune: false
action: true
synopsis: Some extra material for mathcomp
description: |-
Some extra material for mathcomp
[Fibonacci and Lucas numbers](./fib.v)
[Lower bound of lcm(1, 2, ..., n)](./lcm_lbound.v)
[Definitions and some properties of matroids](./matroid.v)
[Rsa algorithm](./rsa.v)
[More lemmas about polynomials](./more_thm.v)
[Polynomials modulo](./divpoly.v)
[Binary gcd](./bgcdn.v)
[Nth root for natural number](./rootn.v)
[The aks algorithm](./aks_algo.v) the algorithm as in Hing Lun Chan's PhD thesis
[The aks correctness proof](./aks.v) a transcription of Hing Lun Chan's proof
[The proof of Lucas theorem for binomial](./digitn.v)
[A formalisation of 2-player games](./tplayer.v) (in progress)
[A formalisation of Fast Fourier Transform](./fft.v)
[More theorems about tuples](./more_tuple.v)
[A formalisation of sorting network](./nsort.v)
[A formalisation of bitonic sort](./bitonic.v)
[A formalisation of Batcher odd or even sort](./batcher.v)
[A formalisation of Knuth exchange sort](./bjsort.v)
[A fun puzzle about a tricky integer function](./puzzleFF.v)
[A port to mathcomp of the elliptic curve of CoqPrime](./elliptic.v)
[A formalisation of some sudoku solvers ](./sudoku.v)
[A formalisation of Montgomery reduction ](./montgomery.v)
[A formalisation of Residue Number System](./rns.v)
[Euler Criterion](./euler.v)
[Trivial fact about the ultra hex number](./ultrahex.v)
A note about sorting network is available [here](https://hal.inria.fr/hal-03585618).
authors:
- name: Laurent Théry
maintainers:
- name: Laurent Théry
nickname: thery
opam-file-maintainer: thery@sophia.inria.fr
license:
fullname: MIT License
identifier: MIT
supported_coq_versions:
text: '8.18 or later'
opam: '{(>= "8.18")}'
dependencies:
- opam:
name: coq-hierarchy-builder
version: '{(>= "1.8.0")}'
description: |-
[ Hierarchy Builder 1.8.0 or later](https://github.com/math-comp/hierarchy-builder)
- opam:
name: coq-mathcomp-ssreflect
version: '{(>= "2.3.0")}'
description: |-
[MathComp ssreflect 2.2.0 or later](https://math-comp.github.io)
- opam:
name: coq-mathcomp-fingroup
version: '{(>= "2.3.0")}'
description: |-
[MathComp fingroup 2.2.0 or later](https://math-comp.github.io)
- opam:
name: coq-mathcomp-algebra
version: '{(>= "2.3.0")}'
description: |-
[MathComp algebra 2.3.0 or later](https://math-comp.github.io)
- opam:
name: coq-mathcomp-field
version: '{(>= "2.3.0")}'
description: |-
[MathComp field 2.3.0 or later](https://math-comp.github.io)
- opam:
name: coq-mathcomp-zify
version: '{(>= "1.5.0+2.0+8.16")}'
description: |-
[MathComp zify 1.5.0+2.0+8.16 or later](https://github.com/math-comp/mczify)
- opam:
name: coq-mathcomp-algebra-tactics
version: '{(>= "1.2.3")}'
description: |-
[MathComp Algebra Tactics 1.2.3 or later](https://github.com/math-comp/algebra-tactics)
tested_coq_opam_versions:
- version: '2.3.0-coq-8.19'
repo: 'mathcomp/mathcomp'
namespace: mathcomp-extra
keywords:
- name: mathcomp extra
---