diff options
| -rw-r--r-- | README.md | 39 |
1 files changed, 24 insertions, 15 deletions
@@ -14,30 +14,39 @@ How to write plugins in Coq In the Coq session type: ```coq - Require Tuto0.Loader. HelloWorld. + Require Import Tuto0.Loader. HelloWorld. ``` # tuto1 : Ocaml to Coq communication 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 - - A command that uses a name and exploits the existing definitions - or theorems - - A command that exploits an existing ongoing proof - - A command that defines a new tactic + - 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 + - A command that uses a name and exploits the existing definitions + or theorems + - A command that exploits an existing ongoing proof + - A command that defines a new tactic + Compilation and loading must be performed as for `tuto0`. + # 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 + - 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 + Compilation and loading must be performed as for `tuto1`. # 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. - - - + Manipulating terms, inside commands and tactics. + - Obtaining existing values from memory + - Composing values + - Verifying types + - Leveraging type inference + - Leveraging coercion + - Using these terms in commands + - Using these terms in tactics + + compilation and loading must be performed as for `tuto0`.
\ No newline at end of file |