meta.yml

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

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

tested_coq_opam_versions:
- version: '2.1.0-coq-8.18'
  repo: 'mathcomp/mathcomp'

namespace: tutorial_material

keywords:
- name: mathematical component
- name: tutorial


---