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