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.

def Lean.Meta.Grind.propagateAndDown : Propagator

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

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.

def Lean.Meta.Grind.propagateOrDown : Propagator

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

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.

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.

def Lean.Meta.Grind.propagateBoolDiseq (a : Expr) : GoalM Unit

def Lean.Meta.Grind.propagateEqUp : Propagator

Propagates Eq upwards

def Lean.Meta.Grind.propagateEqDown : Propagator

Propagates Eq downwards

def Lean.Meta.Grind.propagateBEqUp : Propagator

def Lean.Meta.Grind.propagateBEqDown : Propagator

def Lean.Meta.Grind.propagateEqMatchDown : Propagator

Propagates EqMatch downwards

def Lean.Meta.Grind.propagateHEqDown : Propagator

Propagates HEq downwards

def Lean.Meta.Grind.propagateHEqUp : Propagator

Propagates HEq upwards

def Lean.Meta.Grind.propagateIte : Propagator

Propagates ite upwards

def Lean.Meta.Grind.propagateDIte : Propagator

Propagates dite upwards

def Lean.Meta.Grind.propagateDecideDown : Propagator

def Lean.Meta.Grind.propagateDecideUp : Propagator

def Lean.Meta.Grind.propagateBoolAndUp : Propagator

Bool version of propagateAndUp

def Lean.Meta.Grind.propagateBoolAndDown : Propagator

Bool version of propagateAndDown

def Lean.Meta.Grind.propagateBoolOrUp : Propagator

Bool version of propagateOrUp

def Lean.Meta.Grind.propagateBoolOrDown : Propagator

Bool version of propagateOrDown

def Lean.Meta.Grind.propagateBoolNotUp : Propagator

Bool version of propagateNotUp

def Lean.Meta.Grind.propagateBoolNotDown : Propagator

Bool version of propagateNotDown