Module Checked_ast.Checked0

type ('a, 'f) t =
| Pure : 'a -> ( 'a, 'f ) t
| Direct : ( 'f Run_state.t -> 'f Run_state.t * 'a ) * ( 'a -> ( 'b, 'f ) t ) -> ( 'b, 'f ) t
| Add_constraint : ( 'f Cvar.t, 'f ) Constraint.t * ( 'a, 'f ) t -> ( 'a, 'f ) t
| As_prover : ( unit, 'f ) Types.As_prover.t * ( 'a, 'f ) t -> ( 'a, 'f ) t
| Lazy : ( 'a, 'f ) t * ( 'a Core_kernel.Lazy.t -> ( 'b, 'f ) t ) -> ( 'b, 'f ) t
| With_label : string * ( 'a, 'f ) t * ( 'a -> ( 'b, 'f ) t ) -> ( 'b, 'f ) t
| With_handler : Request.Handler.single * ( 'a, 'f ) t * ( 'a -> ( 'b, 'f ) t ) -> ( 'b, 'f ) t
| Exists : ( 'var, 'value, 'f, ( unit, 'f ) t ) Types.Typ.t * ( ( 'value Request.t, 'f ) Types.As_prover.t, ( 'value, 'f ) Types.As_prover.t ) Types.Provider.t * ( ( 'var, 'value ) Handle.t -> ( 'a, 'f ) t ) -> ( 'a, 'f ) t
| Next_auxiliary : ( int -> ( 'a, 'f ) t ) -> ( 'a, 'f ) t

The type ('ret, 'field, 'runner_state) t represents a checked computation, where

  • 'ret is the return type of the computation
  • 'field is the type of the field elements.