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 list
type 'a embedding =
depth:int ->
Data.hyps ->
Data.constraints ->
Data.state ->
'a ->
Data.state * Data.term * extra_goals
type 'a readback =
depth:int ->
Data.hyps ->
Data.constraints ->
Data.state ->
Data.term ->
Data.state * 'a