Disclaimer: I am no expert or even amateur on this topic.
The Little Prover and The Little Typer might also be of interest. I played some with https://softwarefoundations.cis.upenn.edu/ , and I liked it. It is an interactive textbook. I recommend using it with Emacs (Spacemacs has a coq layer).
Disclaimer: I am no expert or even amateur on this topic.
The Little Prover and The Little Typer might also be of interest. I played some with https://softwarefoundations.cis.upenn.edu/ , and I liked it. It is an interactive textbook. I recommend using it with Emacs (Spacemacs has a coq layer).