Documentation

Lean.Meta.Tactic.Grind.AlphaShareCommon

source
structure Lean.Meta.Grind.AlphaKey :
Type
Instances For
    source
    instance Lean.Meta.Grind.instHashableAlphaKey :
    Hashable AlphaKey
    Equations
      source
      instance Lean.Meta.Grind.instBEqAlphaKey :
      BEq AlphaKey
      Equations
        source
        structure Lean.Meta.Grind.AlphaShareCommon.State :
        Type
        Instances For
          source
          @[reducible, inline]
          abbrev Lean.Meta.Grind.AlphaShareCommonM (α : Type) :
          Type
          Equations
            Instances For
              source
              def Lean.Meta.Grind.shareCommonAlpha (e : Expr) :
              AlphaShareCommonM Expr

              Similar to shareCommon, but handles alpha-equivalence.

              Equations
                Instances For
                  source
                  def Lean.Meta.Grind.shareCommonAlpha.go (e : Expr) :
                  AlphaShareCommonM Expr
                  Equations
                    Instances For