Module Harpoon.Serialization

Module for dealing with Harpoon proof serialization.

val append_sessions : string -> Theorem.t list list -> unit

Appends mutual groups of theorems to the end of the file at the given path. Each `Theorem.t list` represents one session. They are appended in order.

val update_existing_holes : Beluga_syntax.Int.Comp.open_subgoal list -> unit