Module prop::and

Tactics for Logical AND.

Re-exports

pub use commute as symmetry;

Functions

assoc

(a ∧ b) ∧ c => a ∧ (b ∧ c).

commute

a ∧ b => b ∧ a.

distrib

a ∧ (b ∨ c) => (a ∧ b) ∨ (a ∧ c).

exc_both

(¬a ∧ ¬b) ∧ (a ∨ b) => a

exc_left

¬a ∧ (a ∨ b) => b.

exc_right

¬b ∧ (a ∨ b) => a

false_arg

(false ∧ a) => false.

from_de_morgan

¬(a ∨ b) => (¬a ∧ ¬b).

from_imply

¬(a => b) => (a ∧ ¬b).

in_left_arg

(a ∧ b) ∧ (a => c) => (c ∧ b).

in_right_arg

(a ∧ b) ∧ (b => c) => (a ∧ c).

to_de_morgan

(¬a ∧ ¬b) => ¬(a ∨ b).

to_eq_neg

(¬a ∧ ¬b) => (a = b).

to_eq_pos

(a ∧ b) => (a = b).

to_imply

(a ∧ ¬b) => ¬(a => b).

true_arg

(true ∧ a) => true.