Fiche du document
1 juillet 2024
- ISIDORE Id: 10670/1.f863c7...
- hal: hal-04725586
- doi: 10.4204/EPTCS.419.8
Ce document est lié à :
https://inria.hal.science/hal-04550762v2
Ce document est lié à :
info:eu-repo/semantics/altIdentifier/doi/10.4204/EPTCS.419.8
Ce document est lié à :
info:eu-repo/grantAgreement//810367/EU/Extreme-Scale Mathematically-based Computational Chemistry/EMC2
http://creativecommons.org/licenses/by/ , info:eu-repo/semantics/OpenAccess
Mots-clés
Worksheet Coq Arithmetic Divisibility Binomial coefficientSujets proches
School life Students--Education Pupils Student life and customsCiter ce document
Sylvie Boldo et al., « Teaching Divisibility and Binomials with Coq », HAL SHS (Sciences de l’Homme et de la Société), ID : 10.4204/EPTCS.419.8
Métriques
Partage / Export
Résumé
The goal of this contribution is to provide worksheets in Coq for students to learn about divisibility and binomials. These basic topics are a good case study as they are widely taught in the early academic years (or before in France). We present here our technical and pedagogical choices, the numerous exercises we developed and a small experiment we conducted on two students. As expected, it required additional Coq material such as other lemmas and dedicated tactics. The worksheets are freely available and flexible in several ways.
