coq-tutorial-ml-tactics
coq-tutorial-ml-tactics copied to clipboard
Published
20 hours ago •
braibant
braibant
A tutorial on how to write OCaml tactics for the Coq proof assistant
Results
3
coq-tutorial-ml-tactics issues
Sort by
recently updated
recently updated
newest added
Hello, I found an issue where `reflect_arith` in CoqIde wasn't undoing properly. So if I applied `reflect_arith`, went back one step, I would still have the `eval` stuff, then I...
We should add some exercises in a true "Software Foundation" spirit. - For instance, adding support for mult and minus - Adding an example of real reflexive decision/simplification procedure
easy