Tactics

Jump to bottom Edit New page

Catalin Hritcu edited this page Nov 3, 2020 · 4 revisions

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/

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

There are many 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