tutorial_material/meta.yml at master · math-comp/tutorial_material · GitHub

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
---
fullname: tutorial_material
shortname: tutorial_material
organization: math-comp
community: false
dune: false
action: true

synopsis: Scripts associated to tutorials for mathcomp.

description: |-

  ## Tutorial materials

  Scripts associated to tutorials for mathcomp.

  It contains
  - [AnIntroductionToSmallScaleReflectionInCoq](https://github.com/math-comp/tutorial_material/blob/master/AnIntroductionToSmallScaleReflectionInCoq) associated to [An Introduction To Small Scale Reflection In Coq](https://hal.inria.fr/inria-00515548v4/document)
  - [AnSsreflectTutorial](https://github.com/math-comp/tutorial_material/blob/master/AnSsreflectTutorial) associated to [An Ssreflect Tutorial](https://hal.inria.fr/inria-00407778)
  - [SummerSchoolSophia](https://github.com/math-comp/tutorial_material/tree/master/SummerSchoolSophia) associated to a [5-day School](https://team.inria.fr/marelle/en/coq-winter-school-2018/) on Mathematical Components at Sophia-Antipolis


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_rocq_versions:
  text: '9.1 or later'
  opam: '{(>= "9.1")}'

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

tested_coq_opam_versions:
- version: '2.5.0-rocq-prover-9.1'
  repo: 'mathcomp/mathcomp'

namespace: tutorial_material

keywords:
- name: mathematical component
- name: tutorial


---