Module BuiltInPredicate.PPXSource

Sourcetype ('function_type, 'inernal_outtype_in, 'internal_hyps, 'internal_constraints) ffi =
  1. | In : ('t, 'h, 'c) ContextualConversion.t * doc * ('i, 'o, 'h, 'c) ffi -> ('t -> 'i, 'o, 'h, 'c) ffi
  2. | Out : ('t, 'h, 'c) ContextualConversion.t * doc * ('i, 'o * 't option, 'h, 'c) ffi -> ('t oarg -> 'i, 'o, 'h, 'c) ffi
  3. | InOut : ('t ioarg, 'h, 'c) ContextualConversion.t * doc * ('i, 'o * 't option, 'h, 'c) ffi -> ('t ioarg -> 'i, 'o, 'h, 'c) ffi
  4. | Easy : doc -> (depth:int -> 'h -> 'c -> 'o, 'o, 'h, 'c) ffi
  5. | Read : doc -> (depth:int -> 'h -> 'c -> State.t -> 'o, 'o, 'h, 'c) ffi
  6. | Full : doc -> (depth:int -> 'h -> 'c -> State.t -> State.t * 'o * Conversion.extra_goals, 'o, 'h, 'c) ffi
  7. | FullHO : doc -> (once:(depth:int -> term -> State.t -> State.t) -> depth:int -> 'h -> 'c -> State.t -> State.t * 'o * Conversion.extra_goals, 'o, 'h, 'c) ffi
  8. | VariadicIn : ('t, 'h, 'c) ContextualConversion.t * doc -> ('t list -> depth:int -> 'h -> 'c -> State.t -> State.t * 'o * Conversion.extra_goals, 'o, 'h, 'c) ffi
  9. | VariadicOut : ('t, 'h, 'c) ContextualConversion.t * doc -> ('t oarg list -> depth:int -> 'h -> 'c -> State.t -> State.t * ('o * 't option list option) * Conversion.extra_goals, 'o, 'h, 'c) ffi
  10. | VariadicInOut : ('t ioarg, 'h, 'c) ContextualConversion.t * doc -> ('t ioarg list -> depth:int -> 'h -> 'c -> State.t -> State.t * ('o * 't option list option) * Conversion.extra_goals, 'o, 'h, 'c) ffi