val pattern : Gospel.Tterm.pattern -> Ppxlib.patternpattern p translates a Gospel pattern into the matching OCaml pattern
val term : context:Context.t -> Gospel.Tterm.term -> Ppxlib.expressionterm ~context t translates a Gospel typed term into the corresponding OCaml value using the translation context
val term_with_catch :
context:Context.t ->
Gospel.Tterm.term ->
Ppxlib.expressionterm_with_catch ~context t returns the expression generated by term ~context t inside a try ... catch that wraps any raised exception into an Ortac_runtime.Partial_function exception to trace the origin of the exception
val core_type_of_ty_with_subst :
context:Context.t ->
(string -> Ppxlib.core_type option) ->
Gospel.Ttypes.ty ->
Ppxlib.core_typecore_type_of_ty_with_subst subst ty translates a Gospel type into the corresponding OCaml core_type applying subst on the type variables
val core_type_of_tysymbol :
context:Context.t ->
Gospel.Ttypes.tysymbol ->
Ppxlib.core_typecore_type_of_tysymbol ts translates a Gospel type symbol into the corresponding OCaml core_type *