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.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.addDefaultTypeAnalysisLemmas (lemmas : Meta.SimpTheoremsArray) :
        PreProcessM Meta.SimpTheoremsArray
        Equations
        • One or more equations did not get rendered due to their size.
        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