Module Logtk.Defined_pos

Defined positions for Defined Functions

module Fmt = CCFormat
type t =
| P_active
| P_invariant
| 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)
type pos = t
val equal : t -> t -> bool
val pp : Fmt.t -> t -> unit
module Arr : sig ... end