Documentation

Lean.Meta.Tactic.Grind.AC.ToExpr

ToExpr instances for AC types.

source
def Lean.Meta.Grind.AC.ofSeq (m : Grind.AC.Seq) :
Expr
Equations
    Instances For
      source
      instance Lean.Meta.Grind.AC.instToExprSeq :
      ToExpr Grind.AC.Seq
      Equations
        source
        def Lean.Meta.Grind.AC.ofExpr (m : Grind.AC.Expr) :
        Expr
        Equations
          Instances For
            source
            instance Lean.Meta.Grind.AC.instToExprExpr :
            ToExpr Grind.AC.Expr
            Equations