Commit 9368d515 authored by Samuel Ben Hamou's avatar Samuel Ben Hamou
Browse files

Revert "blabla"

This reverts commit afda7aef.
parent afda7aef
......@@ -44,4 +44,3 @@ To be used with Coq 8.8. Just run `make` to compile.
## License
This work is released under the Creative Commons Zero License (CC0). See files [LICENSE](LICENSE) and [COPYING](COPYING) for more.
blabla
expose.pdf
\ No newline at end of file
......@@ -114,6 +114,15 @@ In particular :
## Guided tour of Coq files
## Coq difficulties
- `list term` in the definition of `term`, same in `derivation`
- either `fix 1` or an adhoc induction principle
- A bit of dependent types in models :
- is this graspable by (good) students ?
## Future
To do:
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment