diff --git a/content/blog/coq_docs/index.md b/content/blog/coq_docs/index.md index 2a06e75..bdfc610 100644 --- a/content/blog/coq_docs/index.md +++ b/content/blog/coq_docs/index.md @@ -7,7 +7,7 @@ tags: ["Coq"] --- Recently, I wrote an article on [Formalizing Dawn's Core Calculus in Coq]({{< relref "./coq_dawn.md" >}}). -One of the proofs (specifically, correctness of \\(\\text{quote}_3\\)) was the best candidate I've ever +One of the proofs (specifically, correctness of \(\text{quote}_3\)) was the best candidate I've ever encountered for proof automation. I knew that proof automation was possible from the second book of Software Foundations, [Programming Language Foundations](https://softwarefoundations.cis.upenn.edu/plf-current/index.html). I went there to learn more, and started my little journey in picking up Coq's `Ltac2`.