elpi
ELPI - Embeddable λProlog Interpreter
1024" x-on:close-sidebar="sidebar=window.innerWidth > 1024 && true">
package elpi
-
elpi
-
-
elpi.lexer_config
-
elpi.trace.ppx
-
elpi.trace.runtime
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
Library elpi
type ('a, 'hyps, 'constraints) embedding =
depth:int ->
'hyps ->
'constraints ->
Data.state ->
'a ->
Data.state * Data.term * Conversion.extra_goals
type ('a, 'hyps, 'constraints) readback =
depth:int ->
'hyps ->
'constraints ->
Data.state ->
Data.term ->
Data.state * 'a * Conversion.extra_goals
type ('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_goals
val unit_ctx : ( unit, unit ) ctx_readback
val raw_ctx : ( Data.hyps, Data.constraints ) ctx_readback
val (!<) : ( 'a, unit, unit ) t -> 'a Conversion.t
val (!>) : 'a Conversion.t -> ( 'a, 'hyps, 'constraints ) t
val (!>>) :
( 'a Conversion.t -> 'b Conversion.t ) ->
( 'a, 'hyps, 'constraints ) t ->
( 'b, 'hyps, 'constraints ) t
val (!>>>) :
( 'a Conversion.t -> 'b Conversion.t -> 'c Conversion.t ) ->
( 'a, 'hyps, 'constraints ) t ->
( 'b, 'hyps, 'constraints ) t ->
( 'c, 'hyps, 'constraints ) t
ON THIS PAGE
No table of contents