diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean
index a8db0ee461..c9dbfcaf13 100644
--- a/src/Init/Conv.lean
+++ b/src/Init/Conv.lean
@@ -25,6 +25,7 @@ syntax (name := congr) "congr" : conv
 syntax (name := arg) "arg " num : conv
 syntax (name := ext) "ext " (colGt ident)* : conv
 syntax (name := change) "change " term : conv
+syntax (name := delta) "delta " ident : conv
 syntax (name := pattern) "pattern " term : conv
 syntax (name := rewrite) "rewrite " rwRuleSeq : conv
 syntax (name := erewrite) "erewrite " rwRuleSeq : conv
diff --git a/src/Lean/Elab/Tactic/Conv.lean b/src/Lean/Elab/Tactic/Conv.lean
index 637998311e..42feba3db7 100644
--- a/src/Lean/Elab/Tactic/Conv.lean
+++ b/src/Lean/Elab/Tactic/Conv.lean
@@ -9,3 +9,4 @@ import Lean.Elab.Tactic.Conv.Rewrite
 import Lean.Elab.Tactic.Conv.Change
 import Lean.Elab.Tactic.Conv.Simp
 import Lean.Elab.Tactic.Conv.Pattern
+import Lean.Elab.Tactic.Conv.Delta
diff --git a/src/Lean/Elab/Tactic/Conv/Delta.lean b/src/Lean/Elab/Tactic/Conv/Delta.lean
new file mode 100644
index 0000000000..032618c08a
--- /dev/null
+++ b/src/Lean/Elab/Tactic/Conv/Delta.lean
@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Elab.Tactic.Delta
+import Lean.Elab.Tactic.Conv.Basic
+
+namespace Lean.Elab.Tactic.Conv
+open Meta
+
+@[builtinTactic Lean.Parser.Tactic.Conv.delta] def evalDelta : Tactic := fun stx => withMainContext do
+  let declName ← resolveGlobalConstNoOverload stx[1]
+  let lhsNew ← deltaExpand (← getLhs) (. == declName)
+  changeLhs lhsNew
+
+end Lean.Elab.Tactic.Conv