Notes on hooks into the tactic engine - FStarLang/FStar GitHub Wiki

In flux

1. Work in the c_valedev_initial branch

2. This only works in F# at the moment. So, just build F* using make -C src. You will need a .NET environment, e.g., mono.

To add a new tactic primitive

1. examples/tactics/FStar.Tactics.fst: assume a callback into the compiler; provide the callback at the Tac effect for user programs. Follow the recipe already there for, say, forall_intros

2. In src/tactics/FStar.Tactics.Basic.fs: provide an implementation of the callback

3. In src/tactics/FStar.Tactics.Interpreter.fs install a tactic callback interpretation in primitive_steps