3 ms·

This book is very good. Reading it online is fine, but I highly recommend the curious download it actually run it from your favorite editor

• globuous 6y ago
  Definitely! Otherwise it’s hard to keep track of how each “proof instructions” are manipulating the goals. Definitely give coqide or proofgeneral a try ! By the way, the first chapter is a very good introduction to what formal proving is about ! Last but not least, for all those that are interested in looking into coq, it was very helpful to start learning the basics of Ocaml first (especially variant types) ;)