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

Equations

• Lean.Meta.Grind.instBEqCheckResult = { beq := Lean.Meta.Grind.instBEqCheckResult.beq }

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

Equations

• Lean.Meta.Grind.instBEqCheckResult.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

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

Equations

• Lean.Meta.Grind.instInhabitedCheckResult.default = Lean.Meta.Grind.CheckResult.none

instance Lean.Meta.Grind.instInhabitedCheckResult : Inhabited CheckResult

Equations

• Lean.Meta.Grind.instInhabitedCheckResult = { default := Lean.Meta.Grind.instInhabitedCheckResult.default }

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

Equations

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

instance Lean.Meta.Grind.instReprCheckResult : Repr CheckResult

Equations

• Lean.Meta.Grind.instReprCheckResult = { reprPrec := Lean.Meta.Grind.instReprCheckResult.repr }

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

Equations

• r₁.lt Lean.Meta.Grind.CheckResult.none = false
• Lean.Meta.Grind.CheckResult.none.lt r₂ = true
• r₁.lt Lean.Meta.Grind.CheckResult.progress = false
• Lean.Meta.Grind.CheckResult.progress.lt r₂ = true
• r₁.lt Lean.Meta.Grind.CheckResult.propagated = false
• Lean.Meta.Grind.CheckResult.propagated.lt r₂ = true
• Lean.Meta.Grind.CheckResult.closed.lt Lean.Meta.Grind.CheckResult.closed = false

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

Equations

• r₁.le r₂ = (r₁ == r₂ || r₁.lt r₂)

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

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

Equations

• Lean.Meta.Grind.CheckResult.none.join r₂ = r₂
• r₁.join Lean.Meta.Grind.CheckResult.none = r₁
• Lean.Meta.Grind.CheckResult.progress.join r₂ = r₂
• r₁.join Lean.Meta.Grind.CheckResult.progress = r₁
• Lean.Meta.Grind.CheckResult.propagated.join r₂ = r₂
• r₁.join Lean.Meta.Grind.CheckResult.propagated = r₁
• Lean.Meta.Grind.CheckResult.closed.join Lean.Meta.Grind.CheckResult.closed = Lean.Meta.Grind.CheckResult.closed

Sanity check theorems