4 ms·
F* now has tactics, it is very new, but no doubt that it will evolve a lot... https://github.com/FStarLang/FStar/tree/master/examples/tactics https://github.com
by beurdouche 9y ago
F* now has tactics, it is very new, but no doubt that it will evolve a lot...
https://github.com/FStarLang/FStar/tree/master/examples/tactics https://github.com/FStarLang/FStar/tree/master/examples/tact...
- tom_mellior 9y agoCool! 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).