From a7107aedb382bea1826e9a47d608cf17359a06f5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 18 Nov 2022 08:47:53 -0800
Subject: [PATCH] fix: fixes #1848

---
 src/Lean/Elab/Declaration.lean |  2 +-
 src/Lean/Parser/Command.lean   |  2 +-
 tests/lean/run/1848.lean       | 11 +++++++++++
 3 files changed, 13 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/1848.lean

diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index b8073722b9..f1cf91a4fc 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@@ -190,7 +190,7 @@ def elabClassInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Uni
 def getTerminationHints (stx : Syntax) : TerminationHints :=
   let decl := stx[1]
   let k := decl.getKind
-  if k == ``Parser.Command.def || k == ``Parser.Command.theorem || k == ``Parser.Command.instance then
+  if k == ``Parser.Command.def || k == ``Parser.Command.abbrev || k == ``Parser.Command.theorem || k == ``Parser.Command.instance then
     let args := decl.getArgs
     { terminationBy? := args[args.size - 2]!.getOptional?, decreasingBy? := args[args.size - 1]!.getOptional? }
   else
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index bb61fbcc34..35af9ce35a 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -101,7 +101,7 @@ def declVal          :=
   withAntiquot (mkAntiquot "declVal" `Lean.Parser.Command.declVal (isPseudoKind := true)) <|
     declValSimple <|> declValEqns <|> whereStructInst
 def «abbrev»         := leading_parser
-  "abbrev " >> declId >> ppIndent optDeclSig >> declVal
+  "abbrev " >> declId >> ppIndent optDeclSig >> declVal >> terminationSuffix
 def optDefDeriving   :=
   optional (atomic ("deriving " >> notSymbol "instance") >> sepBy1 ident ", ")
 def «def»            := leading_parser
diff --git a/tests/lean/run/1848.lean b/tests/lean/run/1848.lean
new file mode 100644
index 0000000000..a59b1bdeb9
--- /dev/null
+++ b/tests/lean/run/1848.lean
@@ -0,0 +1,11 @@
+abbrev f : Nat → Nat
+  | 0 => 0
+  | n + 1 => f n
+termination_by _ n => n
+
+mutual
+abbrev f1 : Nat → Nat
+  | 0 => 0
+  | n + 1 => f1 n
+end
+termination_by _ n => n