# Laws

This is a cheatsheet for various terms used to describe laws. Not all of these will appear in Prelude and some may be explained in a type class' definition. Still, it helps to be aware of them:

LawDefinitionExampleExplanation of example
reflexivex function x == true`x <= y``a <= a` is true for any number `a` you pick
irreflexivex function x == false`x < y``a < a` is false for any number `a` you pick
coreflexiveif (x function y) then (x == y)`(x <= 15) && (x == y)`given `(a <= 15) && (a == b)` , then `a == b`
(the converse is not true, though!)
symmetricif (x function y) then (y function x)`x == y`given `a == b`, then `b == a`
antisymmetricif (x function y && y function x) then (x == y)`x <= y`given `a <= b && b <= a`, then `a == b`
asymmetricif (x function y) then (y function x == false)`x < y`given `a < b`, then `!(b < a)`
(asymmetric = anti-symmetric + irreflexive)
transitiveif (x function y && y function z) then (x function z)`x == y`, `x <= y`given `a == b && b == c`, then `a == c`
given `a <= b && b <= c`, then `a <= c`