Literate Theorem Proving with Org

Recently, I've been messing around with Coq. Despite having experience with similar dependently-typed languages/theorem-provers like Agda and Idris, I was intimidated by Coq's "weird" (read: not Haskell-like) syntax and pretty much paid it no attention for a few years. However, I've been increasingly frustrated with the tooling for those languages, which tends to be undocumented and buggy. The situation with Coq, which as far as I know is much more commonly used, seems to be better. Here, I won't focus so much on the language itself but rather on my editor configuration and workflow.

see more

Author: Samuel Breese

Created: 2018-06-15 Fri 00:51