Module `Hint.Morph`

type 'd t constraint 'd = 'l * 'r

Hints that explain morphisms. The allowance 'd describes if the morphism can be on the LHS or RHS of submode.

val id : 'd Hint.Morph.t

The hint for the identity morphism

val left_adjoint : 
  Hint.Pinpoint.t ->
  (_ * Allowance.allowed) Hint.Morph.t ->
  Hint.Pinpoint.t * (Allowance.allowed * Allowance.disallowed) Hint.Morph.t

Given a hint for a mode morphism with its destination pinpoint, return a hint for the left adjoint of the morphism with the opposite pinpoint.

val right_adjoint : 
  Hint.Pinpoint.t ->
  (Allowance.allowed * _) Hint.Morph.t ->
  Hint.Pinpoint.t * (Allowance.disallowed * Allowance.allowed) Hint.Morph.t

Given a hint for a mode morphism with its destination pinpoint, return a hint for the right adjoint of the morphism with the opposite pinpoint.

val unknown : 'd Hint.Morph.t

The hint for unexplained morphs

include Allowance.Allow_disallow with type (_, _, 'd) sided = 'd Hint.Morph.t

type (_, _, 'd) sided = 'd Hint.Morph.t

val disallow_right : 
  ('a, 'b, 'l * 'r) Hint.Morph.sided ->
  ('a, 'b, 'l * Allowance.disallowed) Hint.Morph.sided

Disallows on the right.

val disallow_left : 
  ('a, 'b, 'l * 'r) Hint.Morph.sided ->
  ('a, 'b, Allowance.disallowed * 'r) Hint.Morph.sided

Disallows a the left.

val allow_right : 
  ('a, 'b, 'l * Allowance.allowed) Hint.Morph.sided ->
  ('a, 'b, 'l * 'r) Hint.Morph.sided

Generalizes a right-hand-side allowed to be any allowance.

val allow_left : 
  ('a, 'b, Allowance.allowed * 'r) Hint.Morph.sided ->
  ('a, 'b, 'l * 'r) Hint.Morph.sided

Generalizes a left-hand-side allowed to be any allowance.

Module Hint.Morph

Module `Hint.Morph`