source
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.

Instances For

source
instance Lean.Meta.Grind.instBEqCheckResult :
BEq CheckResult
Equations

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

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

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

Instances For

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

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

Instances For

source
instance Lean.Meta.Grind.instInhabitedCheckResult :
Inhabited CheckResult
Equations

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

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

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

Instances For

source
instance Lean.Meta.Grind.instReprCheckResult :
Repr CheckResult
Equations

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

source
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

Instances For

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

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

Instances For

source
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

Instances For

Sanity check theorems