Web-Projects/blog-static
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Update "I don't like Coq's docs" article to new math delimiters

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-05-13 18:58:15 -07:00
parent 68d9cf1274
commit 6e7ac1c1ca
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
content/blog/coq_docs/index.md
View File

@ -7,7 +7,7 @@ tags: ["Coq"]
--- ---
Recently, I wrote an article on [Formalizing Dawn's Core Calculus in Coq]({{< relref "./coq_dawn.md" >}}). 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 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). 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`. I went there to learn more, and started my little journey in picking up Coq's `Ltac2`.