Safe Haskell | Safe |
---|---|

Language | Haskell2010 |

## Synopsis

- type CounterExample a = Lifted (Op (Set a))
- fmapCounterExample :: (Ord a, Ord b) => (a -> b) -> CounterExample a -> CounterExample b
- counterExample :: e -> CounterExample e
- fromBool :: Ord e => e -> Bool -> CounterExample e
- toBool :: CounterExample e -> Bool
- foldMapCounterExample :: (Ord e, Monoid m) => (e -> m) -> CounterExample e -> Levitated m
- fromCounterExample :: Show a => CounterExample a -> Levitated String
- fromCounterExample' :: Show a => CounterExample a -> Maybe String
- annotate :: Ord e => e -> CounterExample e -> CounterExample e
- (===) :: (Ord e, Eq a) => a -> a -> CounterExample e

# 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

is a Heyting algebra, it is useful in
expressing properties that require assumptions.`CounterExample`

e

fmapCounterExample :: (Ord a, Ord b) => (a -> b) -> CounterExample a -> CounterExample b Source #

counterExample :: e -> CounterExample e Source #

A bijection from `e`

to atoms of the

lattice.`CounterExample`

e

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

A lattice homomorphism from

to `Bool`

, which lifts
`CounterExample`

to an atom of `False`

(uniquely determined by `CounterExample`

`e`

) and
which preserves the top element.

toBool :: CounterExample e -> Bool Source #

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`

.

fromCounterExample :: Show a => CounterExample a -> Levitated String Source #

Map a CounterExample to

. Each set of counter example
is concatenated into a single comma separated string. This is useful for
printing counter examples in tests. See `Levitated`

String

.`fromCounterExample'`

fromCounterExample' :: Show a => CounterExample a -> Maybe String Source #

Map `CounterExample`

to a Maybe, representing

as
`Top`

and mapping both `Nothing`

and `Levitate`

to
a `Bottom`

`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 `\/`

.