This module defines what embedding and readback functions are for datatypes that need the context of the program (hypothetical clauses and constraints)
type ('a, 'hyps, 'constraints) embedding =
depth:int ->
'hyps ->
'constraints ->
Data.state ->
'a ->
Data.state * Data.term * Conversion.extra_goalstype ('a, 'hyps, 'constraints) readback =
depth:int ->
'hyps ->
'constraints ->
Data.state ->
Data.term ->
Data.state * 'a * Conversion.extra_goalstype ('a, 'h, 'c) t = {ty : ty_ast;pp_doc : Format.formatter -> unit -> unit;pp : Format.formatter -> 'a -> unit;embed : ('a, 'h, 'c) embedding;readback : ('a, 'h, 'c) readback;}type ('hyps, 'constraints) ctx_readback =
depth:int ->
Data.hyps ->
Data.constraints ->
Data.state ->
Data.state * 'hyps * 'constraints * Conversion.extra_goalsval unit_ctx : (unit, unit) ctx_readbackval raw_ctx : (Data.hyps, Data.constraints) ctx_readbackval (!<) : ('a, unit, unit) t -> 'a Conversion.tval (!>) : 'a Conversion.t -> ('a, 'hyps, 'constraints) tval (!>>) :
('a Conversion.t -> 'b Conversion.t) ->
('a, 'hyps, 'constraints) t ->
('b, 'hyps, 'constraints) tval (!>>>) :
('a Conversion.t -> 'b Conversion.t -> 'c Conversion.t) ->
('a, 'hyps, 'constraints) t ->
('b, 'hyps, 'constraints) t ->
('c, 'hyps, 'constraints) t