tutorial_material

Tutorial materials

Scripts associated to tutorials for mathcomp.

It contains

• AnIntroductionToSmallScaleReflectionInCoq associated to An Introduction To Small Scale Reflection In Coq
• AnSsreflectTutorial associated to An Ssreflect Tutorial
• SummerSchoolSophia associated to a 5-day School on Mathematical Components at Sophia-Antipolis

Meta

• Author(s):
  • Laurent Théry
• License: MIT License
• Compatible Coq versions: 8.18 or later
• Additional dependencies:
  • MathComp ssreflect 2.1 or later
• Coq namespace: tutorial_material
• Related publication(s): none

Building and installation instructions

The easiest way to install the latest released version of tutorial_material is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-tutorial_material

To instead build and install manually, do:

git clone https://github.com/math-comp/tutorial_material.git
cd tutorial_material
make   # or make -j <number-of-cores-on-your-machine> 
make install