heyting-algebras-0.0.2.0: Heyting and Boolean algebras

Algebra.Heyting.CounterExample

Synopsis

# Documentation

type CounterExample a = Lifted (Op (Set a)) Source #

A counter example type is a Heyting algebra; it useful for tests and properties. It records all failures. The truth value is represented by an empty set. Since CounterExample e is a Heyting algebra, it is useful in expressing properties that require assumptions.

A bijection from e to atoms of the CounterExample e lattice.

fromBool :: Ord e => e -> Bool -> CounterExample e Source #

A lattice homomorphism from Bool to CounterExample, which lifts False to an atom of CounterExample (uniquely determined by e) and which preserves the top element.

A homomorphism of Heyting algebras.

foldMapCounterExample :: (Ord e, Monoid m) => (e -> m) -> CounterExample e -> Levitated m Source #

Note that this map is not a lattice homomorphism (it does not preserve meet nor join). It is also not a poset map in general. Nevertheless, it preserves top and bottom.

Map a CounterExample to Levitated String. Each set of counter example is concatenated into a single comma separated string. This is useful for printing counter examples in tests. See fromCounterExample'.

Map CounterExample to a Maybe, representing Top as Nothing and mapping both Levitate and Bottom to a Just String.

annotate :: Ord e => e -> CounterExample e -> CounterExample e Source #

Add a counter example. This is simply lifts the bottom to an atom given by e, otherwise it preserves the CounterExample e.

Note that take join of e es = counterExample e \/ es will return top if e if e is not in the set es; thus this map is not defined with using \/.

(===) :: (Ord e, Eq a) => a -> a -> CounterExample e infixr 4 Source #