fix: addLValArg

src/Init/Lean/Elab/TermApp.lean

@@ -231,8 +231,8 @@ private def addLValArg (ref : Syntax) (baseName : Name) (fullName : Name) (e : E
     | some idx => do
       let namedArgs := namedArgs.eraseIdx idx;
       addLValArg i namedArgs b
-    | none =>
-      if d.isAppOf baseName then
+    | none => do
+      if d.consumeMData.isAppOf baseName then
         pure $ args.insertAt i (Arg.expr e)
       else if i < args.size then
         addLValArg (i+1) namedArgs b

src/Init/Lean/Expr.lean

@@ -541,6 +541,10 @@ def letName! : Expr → Name
 | letE n _ _ _ _ => n
 | _              => panic! "let expression expected"
 
+def consumeMData : Expr → Expr
+| mdata _ e _ => consumeMData e
+| e           => e
+
 def hasLooseBVars (e : Expr) : Bool :=
 e.looseBVarRange > 0
 

tests/lean/run/frontend1.lean

@@ -177,3 +177,4 @@ f a
 #eval run "universes u v #check Type (max u v)"
 #eval run "#check 'a'"
 #eval fail "#check #['a', \"hello\"]"
+#eval run "#check fun (a : Array Nat) => a.size"