Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package elpi
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
This module defines what embedding and readback functions are
type extra_goals = Data.term listtype 'a embedding =
depth:int ->
Data.hyps ->
Data.constraints ->
Data.state ->
'a ->
Data.state * Data.term * extra_goalstype 'a readback =
depth:int ->
Data.hyps ->
Data.constraints ->
Data.state ->
Data.term ->
Data.state * 'a * extra_goalstype 'a t = {ty : ty_ast;pp_doc : Format.formatter -> unit -> unit;pp : Format.formatter -> 'a -> unit;embed : 'a embedding;readback : 'a readback;
}