Documentation

Lean.Elab.Tactic.BVDecide.Frontend.Normalize.TypeAnalysis

This file implements the type analysis pass for the structures and enum inductives pass. It figures out which types and matches that occur either directly or transitively (e.g. through being contained in a structure) qualify for further treatment by the structures or enum pass.

source
def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.isSupportedMatch (declName : Name) :
MetaM (Option MatchKind)

Determine whether declName is an enum inductive .match_x definition that is supported, see MatchKind for the supported shapes.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.isSupportedMatch.trySimpleEnum (defnInfo : DefinitionVal) (inductiveInfo : InductiveVal) (xs : Array Expr) (numCtors : Nat) (motive : Expr) :
    MetaM (Option MatchKind)
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.isSupportedMatch.verifySimpleCasesOnApp (inductiveInfo : InductiveVal) (fn : Expr) (args params : Array Expr) :
      MetaM Bool
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.isSupportedMatch.verifySimpleEnum (defnInfo : DefinitionVal) (inductiveInfo : InductiveVal) (ctors : Array ConstructorVal) :
        MetaM Bool
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.isSupportedMatch.verifyEnumWithDefault (defnInfo : DefinitionVal) (inductiveInfo : InductiveVal) (ctors : Array ConstructorVal) :
          MetaM Bool
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.builtinTypes :
            Array Name
            Equations
            Instances For
              source
              @[inline]
              def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.isBuiltIn (n : Name) :
              Bool
              Equations
              Instances For
                source
                def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.typeAnalysisPass :
                Pass
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.typeAnalysisPass.checkContext (goal : MVarId) :
                  PreProcessM Unit
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.typeAnalysisPass.analyzeType (expr : Expr) :
                    PreProcessM Unit
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      partial def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.typeAnalysisPass.analyzeConst (n : Name) :
                      PreProcessM Bool

                      Returns true if the const is something that we would like to see revealed by case splitting on structures that contain it.

                      source
                      partial def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.typeAnalysisPass.analyzeStructure (n : Name) :
                      PreProcessM Bool

                      Returns true if the structure is appropriate for case splitting and contains fields of interest.

                      source
                      partial def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.typeAnalysisPass.typeCasesRelevant (expr : Expr) :
                      PreProcessM Bool