Commit afda7aef authored by Samuel Ben Hamou's avatar Samuel Ben Hamou
Browse files


parent 417bb877
......@@ -44,3 +44,4 @@ 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.
\ No newline at end of file
......@@ -114,15 +114,6 @@ 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