3 ms·
Cool! Can you develop them interactively in Emacs, like in Coq, observing how individual tactics change the proof state?
by tom_mellior 9y ago
Cool! Can you develop them interactively in Emacs, like in Coq, observing how individual tactics change the proof state?
- mtzguido 9y agoSadly not yet. You can see each individual intermediate state but the thing runs fully. We certainly plan to add such a feature though! We've been mostly studying hammer-like tactics to, say, apply some theorems at specific places in the goal (which the SMT might be bad at), and not for chaining small rewriting or logical steps (which the SMT is good at).