bool.bend checks

raw source on the hub · import bend-mathlib@0.1.0.1/bool.bend as MBool

1 import

import Base

Laws

law not_not provedsource · line 4 · raw

@b:Bool -> {Bool.not(Bool.not(b)) == b : Bool}

Negating a boolean twice gives it back.

law and_comm provedsource · line 16 · raw

@a:Bool -> @b:Bool -> {Bool.and(a, b) == Bool.and(b, a) : Bool}

Boolean and is commutative.

law or_comm provedsource · line 33 · raw

@a:Bool -> @b:Bool -> {Bool.or(a, b) == Bool.or(b, a) : Bool}

Boolean or is commutative.

law and_assoc provedsource · line 50 · raw

@a:Bool -> @-b:Bool -> @-c:Bool -> {Bool.and(Bool.and(a, b), c) == Bool.and(a, Bool.and(b, c)) : Bool}

Boolean and is associative.

law or_assoc provedsource · line 64 · raw

@a:Bool -> @-b:Bool -> @-c:Bool -> {Bool.or(Bool.or(a, b), c) == Bool.or(a, Bool.or(b, c)) : Bool}

Boolean or is associative.

law and_true provedsource · line 78 · raw

@a:Bool -> {Bool.and(a, True{}) == a : Bool}

True is a right identity for and: a and true is a.

law true_and provedsource · line 90 · raw

@-a:Bool -> {Bool.and(True{}, a) == a : Bool}

True is a left identity for and: true and a is a.

law and_false provedsource · line 98 · raw

@a:Bool -> {Bool.and(a, False{}) == False{} : Bool}

False absorbs and on the right: a and false is false.

law false_and provedsource · line 110 · raw

@-a:Bool -> {Bool.and(False{}, a) == False{} : Bool}

False absorbs and on the left: false and a is false.

law or_false provedsource · line 118 · raw

@a:Bool -> {Bool.or(a, False{}) == a : Bool}

False is a right identity for or: a or false is a.

law false_or provedsource · line 130 · raw

@-a:Bool -> {Bool.or(False{}, a) == a : Bool}

False is a left identity for or: false or a is a.

law or_true provedsource · line 138 · raw

@a:Bool -> {Bool.or(a, True{}) == True{} : Bool}

True absorbs or on the right: a or true is true.

law true_or provedsource · line 150 · raw

@-a:Bool -> {Bool.or(True{}, a) == True{} : Bool}

True absorbs or on the left: true or a is true.

law de_morgan_and provedsource · line 158 · raw

@a:Bool -> @-b:Bool -> {Bool.not(Bool.and(a, b)) == Bool.or(Bool.not(a), Bool.not(b)) : Bool}

De Morgan: not (a and b) is (not a) or (not b).

law de_morgan_or provedsource · line 171 · raw

@a:Bool -> @-b:Bool -> {Bool.not(Bool.or(a, b)) == Bool.and(Bool.not(a), Bool.not(b)) : Bool}

De Morgan: not (a or b) is (not a) and (not b).

law true_ne_false provedsource · line 188 · raw

@_:{True{} == False{} : Bool} -> Empty

True and False are different booleans.

law not_not_sym provedsource · line 197 · raw

@b:Bool -> {b == Bool.not(Bool.not(b)) : Bool}

Negating a boolean twice gives it back, reversed to rewrite toward the simple side.

law and_comm_sym provedsource · line 205 · raw

@a:Bool -> @b:Bool -> {Bool.and(b, a) == Bool.and(a, b) : Bool}

Boolean and is commutative, reversed to rewrite toward the simple side.

law or_comm_sym provedsource · line 214 · raw

@a:Bool -> @b:Bool -> {Bool.or(b, a) == Bool.or(a, b) : Bool}

Boolean or is commutative, reversed to rewrite toward the simple side.

law and_assoc_sym provedsource · line 223 · raw

@a:Bool -> @-b:Bool -> @-c:Bool -> {Bool.and(a, Bool.and(b, c)) == Bool.and(Bool.and(a, b), c) : Bool}

Boolean and is associative, reversed to rewrite toward the simple side.

law or_assoc_sym provedsource · line 233 · raw

@a:Bool -> @-b:Bool -> @-c:Bool -> {Bool.or(a, Bool.or(b, c)) == Bool.or(Bool.or(a, b), c) : Bool}

Boolean or is associative, reversed to rewrite toward the simple side.

law and_true_sym provedsource · line 243 · raw

@a:Bool -> {a == Bool.and(a, True{}) : Bool}

True is a right identity for and: a and true is a, reversed to rewrite toward the simple side.

law true_and_sym provedsource · line 251 · raw

@-a:Bool -> {a == Bool.and(True{}, a) : Bool}

True is a left identity for and: true and a is a, reversed to rewrite toward the simple side.

law and_false_sym provedsource · line 259 · raw

@a:Bool -> {False{} == Bool.and(a, False{}) : Bool}

False absorbs and on the right: a and false is false, reversed to rewrite toward the simple side.

law false_and_sym provedsource · line 267 · raw

@-a:Bool -> {False{} == Bool.and(False{}, a) : Bool}

False absorbs and on the left: false and a is false, reversed to rewrite toward the simple side.

law or_false_sym provedsource · line 275 · raw

@a:Bool -> {a == Bool.or(a, False{}) : Bool}

False is a right identity for or: a or false is a, reversed to rewrite toward the simple side.

law false_or_sym provedsource · line 283 · raw

@-a:Bool -> {a == Bool.or(False{}, a) : Bool}

False is a left identity for or: false or a is a, reversed to rewrite toward the simple side.

law or_true_sym provedsource · line 291 · raw

@a:Bool -> {True{} == Bool.or(a, True{}) : Bool}

True absorbs or on the right: a or true is true, reversed to rewrite toward the simple side.

law true_or_sym provedsource · line 299 · raw

@-a:Bool -> {True{} == Bool.or(True{}, a) : Bool}

True absorbs or on the left: true or a is true, reversed to rewrite toward the simple side.

law de_morgan_and_sym provedsource · line 307 · raw

@a:Bool -> @-b:Bool -> {Bool.or(Bool.not(a), Bool.not(b)) == Bool.not(Bool.and(a, b)) : Bool}

De Morgan: not (a and b) is (not a) or (not b), reversed to rewrite toward the simple side.

law de_morgan_or_sym provedsource · line 316 · raw

@a:Bool -> @-b:Bool -> {Bool.and(Bool.not(a), Bool.not(b)) == Bool.not(Bool.or(a, b)) : Bool}

De Morgan: not (a or b) is (not a) and (not b), reversed to rewrite toward the simple side.

Definitions

def internal_true_ne_false source · line 183 · raw

@e:{True{} == False{} : Bool} -> Empty