diff options
| author | Yves Bertot | 2018-05-08 08:47:58 +0200 |
|---|---|---|
| committer | Yves Bertot | 2018-05-08 08:47:58 +0200 |
| commit | 281fc90700926bd7eb80727bb9e752472d276ba2 (patch) | |
| tree | 22f07f2989a6bcc3ac6e4d2c930243cf96ebfe7d | |
| parent | 69bb967380fe6b461fc542d89408af50d64789d2 (diff) | |
attempt to make code inclusions appear correctly
| -rw-r--r-- | README.md | 24 |
1 files changed, 20 insertions, 4 deletions
@@ -2,18 +2,20 @@ How to write plugins in Coq =========================== # Working environment : merlin, tuareg (open question) # tuto0 : basics of project organization - * package a ml4 file in a plugin, organize a `Makefile`, `_CoqProject` + package a ml4 file in a plugin, organize a `Makefile`, `_CoqProject` - Example of syntax to add a new toplevel command - Example of function call to print a simple message. - To use it: - `cd tuto0; make` - `coqtop -I src -R theories Tuto0` +<pre> + cd tuto0; make + coqtop -I src -R theories Tuto0 +</pre> In the Coq session type: `Require Tuto0.Loader. HelloWorld.` # tuto1 : Ocaml to Coq communication - * Explore the memory of Coq, modify it + Explore the memory of Coq, modify it - Commands that take arguments: strings, symbols, expressions of the calculus of constructions - Commands that interact with type-checking in Coq - A command that adds a new definition or theorem @@ -22,3 +24,17 @@ How to write plugins in Coq - A command that exploits an existing ongoing proof - A command that defines a new tactic + # tuto2 : Ocaml to Coq communication + A more step by step introduction to writing commands + - Explanation of the syntax of entries + - Adding a new type to and parsing to the available choices + - Handling commands that store information in user-chosen registers and tables + + + # tuto3 : manipulating terms of the calculus of constructions + obtaining existing values from memory and composing them, making sure + they are well-typed, and using them in new definitions and proofs. + - + + +
\ No newline at end of file |