diff --git a/src/Init.lean b/src/Init.lean
index d87f6604ad..54741d4ed8 100644
--- a/src/Init.lean
+++ b/src/Init.lean
@@ -18,3 +18,4 @@ import Init.Meta
 import Init.NotationExtra
 import Init.SimpLemmas
 import Init.Hints
+import Init.Conv
diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean
new file mode 100644
index 0000000000..a3b0a290f5
--- /dev/null
+++ b/src/Init/Conv.lean
@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+
+Notation for operators defined at Prelude.lean
+-/
+prelude
+import Init.Notation
+
+namespace Lean.Parser.Tactic
+
+declare_syntax_cat conv (behavior := both)
+
+syntax convSeq1Indented := withPosition((colGe conv ";"?)+)
+syntax convSeqBracketed := "{" (conv ";"?)+ "}"
+syntax convSeq := convSeq1Indented <|> convSeqBracketed
+
+syntax "skip " : conv
+syntax "lhs"   : conv
+syntax "rhs"   : conv
+syntax "whnf"  : conv
+syntax "congr" : conv
+syntax "conv " (" at " ident)? (" in " term)? " => " convSeq : tactic
+
+end Lean.Parser.Tactic
diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index 34716cc4dd..ce12c3a178 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -195,6 +195,7 @@ elab_stx_quot Parser.Term.attr.quot
 elab_stx_quot Parser.Term.prio.quot
 elab_stx_quot Parser.Term.doElem.quot
 elab_stx_quot Parser.Term.dynamicQuot
+-- elab_stx_quot Parser.Term.conv.quot
 
 /- match -/
 
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 4b7db28d8c..91b0ac6c55 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -26,6 +26,9 @@ builtin_initialize
 @[inline] def tacticParser (rbp : Nat := 0) : Parser :=
   categoryParser `tactic rbp
 
+@[inline] def convParser (rbp : Nat := 0) : Parser :=
+  categoryParser `conv rbp
+
 namespace Tactic
 
 def tacticSeq1Indented : Parser :=
@@ -242,6 +245,7 @@ def bracketedBinderF := bracketedBinder  -- no default arg
 @[builtinTermParser] def bracketedBinder.quot : Parser := leading_parser "`(bracketedBinder|"  >> incQuotDepth (evalInsideQuot ``bracketedBinderF bracketedBinder) >> ")"
 @[builtinTermParser] def matchDiscr.quot : Parser := leading_parser "`(matchDiscr|"  >> incQuotDepth (evalInsideQuot ``matchDiscr matchDiscr) >> ")"
 @[builtinTermParser] def attr.quot : Parser := leading_parser "`(attr|"  >> incQuotDepth attrParser >> ")"
+@[builtinTermParser] def conv.quot : Parser := leading_parser "`(conv|"  >> incQuotDepth convParser >> ")"
 
 @[builtinTermParser] def panic       := leading_parser:leadPrec "panic! " >> termParser
 @[builtinTermParser] def unreachable := leading_parser:leadPrec "unreachable!"