Documentation

Sufficient evidence to show that a predicate is either true or false

Forget the evidence payload, yielding just its corresponding boolean value

Evaluate a predicate, yielding either a counterexample or a witness.

The returned value contains the minimum (modulo conjunction/disjunction short circuiting) evidence needed to explain the outcome.

Some examples:

>>> data P = A | B | C deriving Show
>>> a = A := Bool True   -- a ~ True
>>> b = B := 2+2 :==: 5  -- b ~ False
>>> c = C := 10 :>: 5    -- c ~ True

>>> evalPred (a :/\: c) show  -- success because both a~True and c~True
"ETrue ((A := Bool True) :/\\: (C := 10 :>: 5))"

>>> evalPred (a :\/: b) show  -- success because a~True, short-circuits
"ETrue (A := Bool True)"

>>> evalPred (a :/\: b :/\: c) show  -- failure because b~False, short-circuits
"EFalse (B := 4 :==: 5)"

>>> evalPred ((b :\/: a) :/\: (b :\/: c)) show  -- success because of a~True and c~True
"ETrue ((A := Bool True) :/\\: (C := 10 :>: 5))"

>>> evalPred (b :\/: (Not c)) show  -- failure because both b~False and c~True
"EFalse ((B := 4 :==: 5) :\\/: Not (C := 10 :>: 5))"

>>> evalPred (Not (a :/\: b)) show  -- success because b~False
"ETrue (Not (B := 4 :==: 5))"

>>> evalPred (Not (a :/\: c)) show  -- failure because both a~True and c~True
"EFalse (Not ((A := Bool True) :/\\: (C := 10 :>: 5)))"

Provides a human-readable explanation for a value

Explanation mode

Used to control whether we want to continue explaining terms beyond tags * Shallow: only explain tags * Deep: explain full predicates

Default Explainable instance via Show to be used with 'deriving via'

Shallow explanation

Deep explanation