A Small Scale Reflection Extension for the Coq system

Abstract : This is the user manual of Ssreflect, a set of extensions to the proof scripting language of the Coq proof assistant. While these extensions were developed to support a particular proof methodology - small-scale reflection - most of them actually are of a quite general nature, improving the functionality of Coq in basic areas such as script layout and structuring, proof context management, and rewriting. Consequently, and in spite of the title of this document, most of the extensions described here should be of interest for all Coq users, whether they embrace small-scale reflection or not.
Type de document :
Rapport
[Research Report] RR-6455, Inria Saclay Ile de France. 2016
Liste complète des métadonnées

https://hal.inria.fr/inria-00258384
Contributeur : Assia Mahboubi <>
Soumis le : jeudi 3 novembre 2016 - 14:00:53
Dernière modification le : samedi 18 février 2017 - 01:14:43
Document(s) archivé(s) le : samedi 4 février 2017 - 13:39:45

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00258384, version 17

Citation

Georges Gonthier, Assia Mahboubi, Enrico Tassi. A Small Scale Reflection Extension for the Coq system. [Research Report] RR-6455, Inria Saclay Ile de France. 2016. <inria-00258384v17>

Partager

Métriques

Consultations de
la notice

825

Téléchargements du document

431