Module prop::or

Tactics for Logical OR.

Re-exports

pub use commute as symmetry;

Functions

assoc

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

bound_neg

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

bound_pos

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

commute

a ∨ b => b ∨ a.

distrib

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

from_de_morgan

¬(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).