.. _harpoon:

Interactive Proving with Harpoon
================================

Harpoon is an interactive prover for Beluga. Users of Harpoon develop proofs in
a REPL using a small set of built-in tactics. These correspond to the main proof
strategies one uses in developing metatheory proofs, e.g. inversion or appeal to
a lemma or induction hypothesis.

.. toctree::
   :maxdepth: 2

   prover-structure
   proof-automation
   interactive-reference
   undo