Module Syncom.Inductivity

Annotations for parameters and variables generating induction hypotheses.

type t = private
  1. | Inductive
    (*

    The annotation for inductive parameters.

    *)
  2. | Not_inductive
    (*

    The annotation for non-inductive parameters.

    *)

The type of annotation for inductive or not inductive parameters.

An inductive parameter generates induction hypotheses when split on.

Constructors

val not_inductive : t

not_inductive is Not_inductive.

val inductive : t

inductive is Inductive.

Predicates and comparisons

val max : t -> t -> t

max ind1 ind2 is Inductive if at least one of ind1 and ind2 is Inductive. Otherwise, Not_inductive is returned.

val min : t -> t -> t

min ind1 ind2 is Not_inductive if at least one of ind1 and ind2 is Not_inductive. Otherwise, Inductive is returned.

val is_not_inductive : t -> bool

is_not_inductive ind is true if and only if ind is Not_inductive.

val is_inductive : t -> bool

is_inductive ind is true if and only if ind is Inductive.

Instances

include Support.Eq.EQ with type t := t
val equal : t -> t -> bool

equal a b is true if and only if a and b are equal. This should satisfy the following properties:

  • Reflexivity: equal a a = true
  • Symmetry: equal a b is equivalent to equal b a
  • Transitivity: if equal a b = true and equal b c = true, then equal a c = true
val (=) : t -> t -> bool

Operator alias of equal.

val (<>) : t -> t -> bool

Negation of operator (=).