Action (beluga.Harpoon.Theorem.Action)

type t

Abstract actions that can be executed forwards and backwards on a theorem.

val make : 
  string ->
  Synint.Comp.proof_state ->
  Synint.Comp.proof_state list ->
  Synint.Comp.proof ->
  t

An action describes a diff on the subgoals of the theorem.

In the forward direction, it assigns the solution to the target subgoal, removes the target, and adds all child subgoals.
In the backward direction, it removes all child subgoals, adds the target, and clears the solution of the target.

val name_of_action : t -> string