From 6e7ac1c1cabd815ec7b73a3daa110a147d9acfa2 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Mon, 13 May 2024 18:58:15 -0700 Subject: [PATCH] Update "I don't like Coq's docs" article to new math delimiters Signed-off-by: Danila Fedorin --- content/blog/coq_docs/index.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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`.