package fix

  1. Overview
  2. Docs
package fix
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Prop.BooleanSource

The lattice of Booleans.

The Boolean lattice. The ordering is false <= true.

Sourcetype property = bool
Sourceval bottom : property
Sourceval equal : property -> property -> bool
Sourceval is_maximal : property -> bool
Sourceval leq : bool -> bool -> bool
Sourceval join : bool -> bool -> bool
Sourceval leq_join : bool -> bool -> bool

leq_join p q must compute the join of p and q. If the result is logically equal to q, then q itself must be returned. Thus, we have leq_join p q == q if and only if leq p q holds.