What tactic languages and declarative proof languages exist for different proof assistants? I'm interested in anything from common to obscure, in any proof assistant, at any time in history, including the ML family of languages when used to implement tactics and tacticals.
-
-
Ah, I read this before I had any idea what I was reading. It looks like this is what inspired the Lean tactic monad. Thanks!
-
I think the Lean folks were having similar ideas before they knew what I was doing. But they definitely improved on my work in many ways, like a debugger and profiler and better representation of quoted terms.
End of conversation
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.