From f95675dc22d8a49e4a161bd61573f3371285b99b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 14 Sep 2020 14:25:35 -0700
Subject: [PATCH] feat: add `have-by` and `show-by` syntax

---
 src/Lean/Parser/Term.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 1aa184939b..6197d739ea 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -45,6 +45,8 @@ def leadPrec := maxPrec - 1
 
 /- Built-in parsers -/
 
+@[builtinTermParser] def byTactic := parser!:maxPrec "by " >> Tactic.indentedNonEmptySeq
+
 -- `checkPrec` necessary for the pretty printer
 @[builtinTermParser] def ident := checkPrec maxPrec >> Parser.ident
 @[builtinTermParser] def num : Parser := checkPrec maxPrec >> numLit
@@ -67,11 +69,11 @@ def optIdent : Parser := optional (try (ident >> " : "))
 @[builtinTermParser] def «if»  := parser!:leadPrec "if " >> optIdent >> termParser >> " then " >> termParser >> " else " >> termParser
 def fromTerm   := parser! " from " >> termParser
 def haveAssign := parser! " := " >> termParser
-def haveDecl   := optIdent >> termParser >> (haveAssign <|> fromTerm)
+def haveDecl   := optIdent >> termParser >> (haveAssign <|> fromTerm <|> byTactic)
 @[builtinTermParser] def «have» := parser!:leadPrec "have " >> haveDecl >> "; " >> termParser
 def sufficesDecl := optIdent >> termParser >> fromTerm
 @[builtinTermParser] def «suffices» := parser!:leadPrec "suffices " >> sufficesDecl >> "; " >> termParser
-@[builtinTermParser] def «show»     := parser!:leadPrec "show " >> termParser >> fromTerm
+@[builtinTermParser] def «show»     := parser!:leadPrec "show " >> termParser >> (fromTerm <|> byTactic)
 def structInstArrayRef := parser! "[" >> termParser >>"]"
 def structInstLVal   := (ident <|> fieldIdx <|> structInstArrayRef) >> many (group ("." >> (ident <|> fieldIdx)) <|> structInstArrayRef)
 def structInstField  := parser! structInstLVal >> " := " >> termParser
@@ -242,8 +244,6 @@ stx.isAntiquot || stx.isIdent
 @[builtinTermParser] def seqRight    := tparser! infixR " *> "  60
 @[builtinTermParser] def map         := tparser! infixR " <$> " 100
 
-@[builtinTermParser] def byTactic    := parser!:maxPrec "by " >> Tactic.indentedNonEmptySeq
-
 @[builtinTermParser] def funBinder.quot : Parser := parser! "`(funBinder|"  >> toggleInsideQuot funBinder >> ")"
 
 @[builtinTermParser] def panic       := parser!:leadPrec "panic! " >> termParser