def Lean.Meta.Grind.propagateAndUp : Propagator

Propagates equalities for a conjunction a ∧ b based on the truth values of its components a and b. This function checks the truth value of a and b, and propagates the following equalities:

• If a = True, propagates (a ∧ b) = b.
• If b = True, propagates (a ∧ b) = a.
• If a = False, propagates (a ∧ b) = False.
• If b = False, propagates (a ∧ b) = False.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.propagateAndDown : Propagator

Propagates truth values downwards for a conjunction a ∧ b when the expression itself is known to be True.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.propagateOrUp : Propagator

Propagates equalities for a disjunction a ∨ b based on the truth values of its components a and b. This function checks the truth value of a and b, and propagates the following equalities:

• If a = False, propagates (a ∨ b) = b.
• If b = False, propagates (a ∨ b) = a.
• If a = True, propagates (a ∨ b) = True.
• If b = True, propagates (a ∨ b) = True.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.propagateOrDown : Propagator

Propagates truth values downwards for a disjuction a ∨ b when the expression itself is known to be False.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.propagateNotUp : Propagator

Propagates equalities for a negation Not a based on the truth value of a. This function checks the truth value of a and propagates the following equalities:

• If a = False, propagates (Not a) = True.
• If a = True, propagates (Not a) = False.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.propagateNotDown : Propagator

Propagates truth values downwards for a negation expression Not a based on the truth value of Not a. This function performs the following:

• If (Not a) = False, propagates a = True.
• If (Not a) = True, propagates a = False.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.propagateEqUp : Propagator

Propagates Eq upwards

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.propagateEqDown : Propagator

Propagates Eq downwards

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.propagateHEqDown : Propagator

Propagates HEq downwards

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.propagateHEqUp : Propagator

Propagates HEq upwards

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.propagateIte : Propagator

Propagates ite upwards

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.propagateDIte : Propagator

Propagates dite upwards

Equations

• One or more equations did not get rendered due to their size.