chore: naming

src/Init/Meta.lean

@@ -142,12 +142,15 @@ instance monadNameGeneratorLift (m n : Type → Type) [MonadLift m n] [MonadName
 
 namespace Syntax
 
-partial def getTailInfo : Syntax → Option SourceInfo
+partial def getTailInfo? : Syntax → Option SourceInfo
   | atom info _   => info
   | ident info .. => info
-  | node _ args   => args.findSomeRev? getTailInfo
+  | node _ args   => args.findSomeRev? getTailInfo?
   | _             => none
 
+def getTailInfo (stx : Syntax) : SourceInfo :=
+  stx.getTailInfo?.getD SourceInfo.none
+
 @[specialize] private partial def updateLast {α} [Inhabited α] (a : Array α) (f : α → Option α) (i : Nat) : Option (Array α) :=
   if i == 0 then
     none

src/Lean/Parser/Basic.lean

@@ -1081,8 +1081,8 @@ def symbolInfo (sym : String) : ParserInfo := {
 
 def checkTailNoWs (prev : Syntax) : Bool :=
   match prev.getTailInfo with
-  | some (SourceInfo.original _ _ trailing) => trailing.stopPos == trailing.startPos
-  | _                                       => false
+  | SourceInfo.original _ _ trailing => trailing.stopPos == trailing.startPos
+  | _                                => false
 
 /-- Check if the following token is the symbol _or_ identifier `sym`. Useful for
     parsing local tokens that have not been added to the token table (but may have
@@ -1135,8 +1135,8 @@ partial def strAux (sym : String) (errorMsg : String) (j : Nat) :ParserFn :=
 
 def checkTailWs (prev : Syntax) : Bool :=
   match prev.getTailInfo with
-  | some (SourceInfo.original _ _ trailing) => trailing.stopPos > trailing.startPos
-  | _                                       => false
+  | SourceInfo.original _ _ trailing => trailing.stopPos > trailing.startPos
+  | _                                => false
 
 def checkWsBeforeFn (errorMsg : String) : ParserFn := fun c s =>
   let prev := s.stxStack.back