Documentation

Lean.Meta.Tactic.Grind.CheckResult

source
inductive Lean.Meta.Grind.CheckResult :
Type

Result type for satisfiability checking procedures.

Instances For
    source
    @[implicit_reducible]
    instance Lean.Meta.Grind.instBEqCheckResult :
    BEq CheckResult
    source
    def Lean.Meta.Grind.instBEqCheckResult.beq :
    CheckResult → CheckResult → Bool
    Instances For
      source
      def Lean.Meta.Grind.instInhabitedCheckResult.default :
      CheckResult
      Instances For
        source
        @[implicit_reducible]
        instance Lean.Meta.Grind.instInhabitedCheckResult :
        Inhabited CheckResult
        source
        def Lean.Meta.Grind.instReprCheckResult.repr :
        CheckResult → Nat → Format
        Instances For
          source
          @[implicit_reducible]
          instance Lean.Meta.Grind.instReprCheckResult :
          Repr CheckResult
          source
          def Lean.Meta.Grind.CheckResult.lt (r₁ r₂ : CheckResult) :
          Bool
          Instances For
            source
            def Lean.Meta.Grind.CheckResult.le (r₁ r₂ : CheckResult) :
            Bool
            Instances For
              source
              def Lean.Meta.Grind.CheckResult.join (r₁ r₂ : CheckResult) :
              CheckResult

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

              Instances For

                Sanity check theorems