From 79c15de131a50ed970be65f4debc7207fbca0baa Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 24 Dec 2020 07:54:20 -0800
Subject: [PATCH] fix: `if-then-else` is not builtin notation

---
 src/Lean/Elab/Quotation.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index a02747c653..9c400f6368 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -254,7 +254,7 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
                 covered (adaptRhs rhsFn ∘ noOpMatchAdaptPats taken) (exhaustive := sz.isNone)
               else uncovered
             | _ => uncovered,
-          doMatch := fun yes no => do `(if Syntax.isOfKind discr $(quote k) then $(← yes []) else $(← no)),
+          doMatch := fun yes no => do `(cond (Syntax.isOfKind discr $(quote k)) $(← yes []) $(← no)),
         }
       else throwErrorAt! anti "match_syntax: antiquotation must be variable {anti}"
     else if isAntiquotSuffixSplice quoted then throwErrorAt quoted "unexpected antiquotation splice"