Module `Solver_mono.Unhint`Source

Sourcetype ('a, 'd) t constraint 'd = 'l * 'r

Unhinted mode is similar to ('a, 'd) mode, but its several outermost morphism applications are unhinted.

Sourceval unhint : ('a, 'l * 'r) mode -> ('a, 'l * 'r) t

Treat a regular mode as an unhinted mode, by taking the identity morphism as the outermost unhinted morphism.

val hint : 
  'a C.obj ->
  ?hint:('l * 'r) Hint.Morph.t ->
  ('a, 'l * 'r) t ->
  ('a, 'l * 'r) mode

Takes an unhinted mode, annotate the outermost unhinted morphisms (as a whole) with the given hint, which gives a regular mode.

val apply : 
  'b C.obj ->
  ('a, 'b, 'l * 'r) C.morph ->
  ('a, 'l * 'r) t ->
  ('b, 'l * 'r) t

Apply another unhinted morphism to an unhinted mode.

Module Solver_mono.UnhintSource