Tactics

Paper on tactics: https://arxiv.org/pdf/1803.06547.pdf

Jonathan Protzenko lecture at Dagstuhl: https://www.cl.cam.ac.uk/events/metaprog/2019/lectures.html

Some demos with comments https://jonathan.protzenko.fr/courses/dagstuhl2019/

Some commented files illustrating tactics from ECI 2019 summer school: https://www.fstar-lang.org/eci2019/meta/Term.fst https://www.fstar-lang.org/eci2019/meta/Metaprogramming.fst

A previous course by Danel Ahman: https://danel.ahman.ee/teaching/taltech2018/index.html

There are many more examples of tactic usage in

https://github.com/FStarLang/FStar/tree/master/examples/tactics

https://github.com/FStarLang/FStar/blob/master/ulib/FStar.Tactics.Sequences.fst with notes at the bottom of the file

https://github.com/FStarLang/FStar/tree/master/examples/tactics especially Synthesis and Printers

https://github.com/project-everest/hacl-star/blob/master/code/meta/

https://github.com/project-everest/hacl-star/blob/master/providers/test/Test.Lowstarize.fst