From 4768ac2fbcda11ce6237ed226af9c1d0ff5b7aa7 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 19 Aug 2020 14:59:18 +0200
Subject: [PATCH] chore: make `Syntax.getArg(s)` panic

---
 src/Init/LeanInit.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Init/LeanInit.lean b/src/Init/LeanInit.lean
index cdb8c968e6..c76f92ad11 100644
--- a/src/Init/LeanInit.lean
+++ b/src/Init/LeanInit.lean
@@ -223,12 +223,12 @@ def isOfKind : Syntax → SyntaxNodeKind → Bool
 def getArg (stx : Syntax) (i : Nat) : Syntax :=
 match stx with
 | Syntax.node _ args => args.get! i
-| _                  => arbitrary _
+| _                  => panic! "Syntax.getArg: not a node"
 
 def getArgs (stx : Syntax) : Array Syntax :=
 match stx with
 | Syntax.node _ args => args
-| _                  => #[]
+| _                  => panic! "Syntax.getArgs: not a node"
 
 /-- Retrieve the left-most leaf's info in the Syntax tree. -/
 partial def getHeadInfo : Syntax → Option SourceInfo