Module Harpoon

module Automation : sig ... end
module CidProgRewrite : sig ... end

Contains a family a functions for rewriting references to program functions.

module HarpoonState : sig ... end
module InputPrompt : sig ... end
module Io : sig ... end

Centralizes high-level Harpoon input-output capabilities.

module Options : sig ... end
module Prover : sig ... end
module Repl : sig ... end

Main Harpoon REPL module.

module Revisit : sig ... end
module Serialization : sig ... end

Module for dealing with Harpoon proof serialization.

module Session : sig ... end
module Tactic : sig ... end

All the high-level proof tactics. * In general, a tactic has inputs * 1. Some tactic-specific parameters * 2. A `proof_state` to act on * * Tactics are parameterized by a TacticContext that gives them * certain capabilities, such as manipulating the subgoal list or * showing messages to the user. * * Tactics are not obligated to solve the current subgoal!

module Theorem : sig ... end
module Translate : sig ... end