inductive Lean.Meta.Grind.CheckResult : Type

Result type for satisfiability checking procedures.

• none : CheckResult

  No progress

• progress : CheckResult

  Updated basis, simplified equations.

• propagated : CheckResult

  Propagated equations back to the core.

• closed : CheckResult

  Closed the goal.

instance Lean.Meta.Grind.instBEqCheckResult : BEq CheckResult

def Lean.Meta.Grind.instBEqCheckResult.beq : CheckResult → CheckResult → Bool

def Lean.Meta.Grind.instInhabitedCheckResult.default : CheckResult

instance Lean.Meta.Grind.instInhabitedCheckResult : Inhabited CheckResult

def Lean.Meta.Grind.instReprCheckResult.repr : CheckResult → Nat → Format

instance Lean.Meta.Grind.instReprCheckResult : Repr CheckResult

def Lean.Meta.Grind.CheckResult.lt (r₁ r₂ : CheckResult) : Bool

def Lean.Meta.Grind.CheckResult.le (r₁ r₂ : CheckResult) : Bool

def Lean.Meta.Grind.CheckResult.join (r₁ r₂ : CheckResult) : CheckResult

Joins two results. It uses the order .none < .progress < .propagated < .closed

Sanity check theorems