diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index a85559992f..1e026ee763 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -648,6 +648,10 @@ partial def evalPrec : Syntax → MacroM Nat
 
 macro "evalPrec! " p:prec:max : term => return quote (← evalPrec p)
 
+def evalOptPrec : Option Syntax → MacroM Nat
+  | some prec => evalPrec prec
+  | none      => return 0
+
 end Lean
 
 namespace Array
diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index 17ae271e53..2d337b5c49 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -382,14 +382,12 @@ def elabNoKindMacroRulesAux (alts : Array Syntax) : CommandElabM Syntax := do
 
 -- TODO: cleanup after we have support for optional syntax at `match_syntax`
 @[builtinMacro Lean.Parser.Command.mixfix] def expandMixfix : Macro := fun stx =>
-  withAttrKindGlobal stx fun stx =>
+  withAttrKindGlobal stx fun stx => do
     match stx with
     | `(infix $[: $prec]? $[[$prio]]? $op => $f)   => `(infixl $[: $prec]? $[[$prio]]? $op => $f)
     | `(infixr $[: $prec]? $[[$prio]]? $op => $f)  => `(notation $[: $prec]? $[[$prio]]? lhs $op:strLit rhs $[: $prec]? => $f lhs rhs)
     | `(infixl $[: $prec]? $[[$prio]]? $op => $f)  =>
-       let prec1 : Syntax := match (prec : Option Syntax) with
-         | some prec => quote (prec.toNat+1)
-         | none      => quote 0
+       let prec1 := quote <| (← evalOptPrec prec) + 1
        `(notation $[: $prec]? $[[$prio]]? lhs $op:strLit rhs:$prec1 => $f lhs rhs)
     | `(prefix $[: $prec]? $[[$prio]]? $op => $f)  => `(notation $[: $prec]? $[[$prio]]? $op:strLit arg $[: $prec]? => $f arg)
     | `(postfix $[: $prec]? $[[$prio]]? $op => $f) => `(notation $[: $prec]? $[[$prio]]? arg $op:strLit => $f arg)
diff --git a/tests/lean/run/precDSL.lean b/tests/lean/run/precDSL.lean
new file mode 100644
index 0000000000..d933758a62
--- /dev/null
+++ b/tests/lean/run/precDSL.lean
@@ -0,0 +1,28 @@
+syntax:max "fn " ident "=>" term : term
+syntax:(lead+1) "function " ident "=>" term : term
+
+macro_rules
+  | `(fn $x:ident => $b) => `(fun $x:ident => $b)
+  | `(function $x:ident => $b) => `(fun $x:ident => $b)
+
+#check id fn x => x + 1
+#check id function x => x + 1
+
+macro "addPrec" : prec => `(65)
+macro "mulPrec" : prec => `(70)
+
+infix:addPrec " +' " => Nat.add
+infix:mulPrec " *' " => Nat.mul
+
+#eval 10 +' 2 *' 3
+
+theorem ex1 : 10 +' 2 *' 3 = 16 :=
+  rfl
+
+theorem ex2 : 10 + 2 * 3 = 16 :=
+  rfl
+
+infix:(addPrec-1) " *'' " => Nat.mul
+
+theorem ex3 : 10 +' 2 *'' 3 = 36 :=
+  rfl