package elpi

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module API.ConversionSource

This module defines what embedding and readback functions are

Sourcetype ty_ast =
  1. | TyName of string
  2. | TyApp of string * ty_ast * ty_ast list
Sourcetype extra_goal = ..
Sourcetype extra_goal +=
  1. | Unify of Data.term * Data.term
Sourcetype extra_goals = extra_goal list
Sourcetype 'a embedding = depth:int -> Data.state -> 'a -> Data.state * Data.term * extra_goals
Sourcetype 'a readback = depth:int -> Data.state -> Data.term -> Data.state * 'a * extra_goals
Sourcetype 'a t = {
  1. ty : ty_ast;
  2. pp_doc : Format.formatter -> unit -> unit;
  3. pp : Format.formatter -> 'a -> unit;
  4. embed : 'a embedding;
  5. readback : 'a readback;
}
Sourceexception TypeErr of ty_ast * int * Data.term
OCaml

Innovation. Community. Security.