Harpoon.Translateexception Error of errortype result = (error, Synint.Comp.exp) Support.Either.tval entry : Beluga.Store.Cid.Comp.Entry.t -> resultTranslates a theorem given by a Store entry.
val theorem : Synint.Comp.thm -> Synint.Comp.typ -> Synint.Comp.expTranslates a theorem. Theorems proven already by a program are returned as-is, but theorems proven with a Harpoon proof are translated.
val trap : (unit -> 'a) -> (error, 'a) Support.Either.tTraps exceptions raised by this module.
val fmt_ppr_error : Support.Format.formatter -> error -> unitFormats an error.
val fmt_ppr_result : Support.Format.formatter -> result -> unitFormats a translation result.