Module Logtk.Defined_posSource

Defined positions for Defined Functions

Sourcemodule Fmt = CCFormat
Sourcetype t =
  1. | P_active
  2. | P_invariant
  3. | P_accumulator

positions that are immediate arguments of some defined constant can be classified as follows:

  • active position (patterns on LHS of rules)
  • invariant positions (variable on LHS and RHS of rules)
  • accumulator positions (variable on LHS, non-variable on RHS)
Sourcetype pos = t
Sourceval equal : t -> t -> bool
Sourceval pp : Fmt.t -> t -> unit
Sourcemodule Arr : sig ... end