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
Instances For
    source
    def Lean.Grind.AC.Expr.denoteExpr {M : Type → Type} [Monad M] [Meta.Grind.AC.MonadGetStruct M] (e : Expr) :
    M Lean.Expr
    Instances For
      source
      def Lean.Meta.Grind.AC.EqCnstr.denoteExpr {M : Type → Type} [Monad M] [MonadGetStruct M] (c : EqCnstr) :
      M Expr
      Instances For
        source
        def Lean.Meta.Grind.AC.DiseqCnstr.denoteExpr {M : Type → Type} [Monad M] [MonadGetStruct M] (c : DiseqCnstr) :
        M Expr
        Instances For