elpi 1.8.0 · OCaml Package

exception No_clause

type name = string

type doc = string

type 'a oarg =

| Keep
| Discard

type 'a ioarg =

| Data of 'a
| NoData

type ('function_type, 'inernal_outtype_in, 'internal_hyps, 'internal_constraints)
  ffi =

| In : 't Conversion.t * doc * ('i, 'o, 'h, 'c) ffi -> ('t -> 'i, 'o, 'h, 'c) ffi
| Out : 't Conversion.t * doc * ('i, 'o * 't option, 'h, 'c) ffi -> ('t oarg -> 'i, 'o, 'h, 'c) ffi
| InOut : 't Conversion.t * doc * ('i, 'o * 't option, 'h, 'c) ffi -> ('t ioarg -> 'i, 'o, 'h, 'c) ffi
| CIn : ('t, 'h, 'c) ContextualConversion.t * doc * ('i, 'o, 'h, 'c) ffi -> ('t -> 'i, 'o, 'h, 'c) ffi
| COut : ('t, 'h, 'c) ContextualConversion.t * doc * ('i, 'o * 't option, 'h, 'c) ffi -> ('t oarg -> 'i, 'o, 'h, 'c) ffi
| CInOut : ('t, 'h, 'c) ContextualConversion.t * doc * ('i, 'o * 't option, 'h, 'c) ffi -> ('t ioarg -> 'i, 'o, 'h, 'c) ffi
| Easy : doc -> (depth:int -> 'o, 'o, unit, unit) ffi
| Read : ('h, 'c) ContextualConversion.ctx_readback * doc -> (depth:int -> 'h -> 'c -> Data.state -> 'o, 'o, 'h, 'c) ffi
| Full : ('h, 'c) ContextualConversion.ctx_readback * doc -> (depth:int -> 'h -> 'c -> Data.state -> Data.state * 'o * Conversion.extra_goals, 'o, 'h, 'c) ffi
| VariadicIn : ('h, 'c) ContextualConversion.ctx_readback * ('t, 'h, 'c) ContextualConversion.t * doc -> ('t list -> depth:int -> 'h -> 'c -> Data.state -> Data.state * 'o, 'o, 'h, 'c) ffi
| VariadicOut : ('h, 'c) ContextualConversion.ctx_readback * ('t, 'h, 'c) ContextualConversion.t * doc -> ('t oarg list -> depth:int -> 'h -> 'c -> Data.state -> Data.state * ('o * 't option list option), 'o, 'h, 'c) ffi
| VariadicInOut : ('h, 'c) ContextualConversion.ctx_readback * ('t, 'h, 'c) ContextualConversion.t * doc -> ('t ioarg list -> depth:int -> 'h -> 'c -> Data.state -> Data.state * ('o * 't option list option), 'o, 'h, 'c) ffi

type t =

| Pred : name * ('a, unit, 'h, 'c) ffi * 'a -> t

module Notation : sig ... end

package elpi