Documentation

Lean.Meta.Tactic.Grind.AC.DenoteExpr

source
def Lean.Grind.AC.Seq.denoteExpr {M : Type → Type} [Monad M] [Meta.Grind.AC.MonadGetStruct M] (s : Seq) :
M Lean.Expr
Equations
    Instances For
      source
      def Lean.Grind.AC.Expr.denoteExpr {M : Type → Type} [Monad M] [Meta.Grind.AC.MonadGetStruct M] (e : Expr) :
      M Lean.Expr
      Equations
        Instances For
          source
          def Lean.Meta.Grind.AC.EqCnstr.denoteExpr {M : Type → Type} [Monad M] [MonadGetStruct M] (c : EqCnstr) :
          M Expr
          Equations
            Instances For
              source
              def Lean.Meta.Grind.AC.DiseqCnstr.denoteExpr {M : Type → Type} [Monad M] [MonadGetStruct M] (c : DiseqCnstr) :
              M Expr
              Equations
                Instances For