chore: goodies for deriving command

src/Init/Data/Array/Subarray.lean

@@ -112,3 +112,9 @@ macro_rules
   | `($a[$start : ])      => `(let a := $a; Array.toSubarray a $start a.size)
 
 end Array
+
+def Subarray.toArray (s : Subarray α) : Array α :=
+  Array.ofSubarray s
+
+instance : HAppend (Subarray α) (Subarray α) (Array α) where
+  hAppend x y := x.toArray ++ y.toArray

src/Init/Data/String/Basic.lean

@@ -518,6 +518,9 @@ def trim (s : String) : String :=
 def capitalize (s : String) :=
   s.set 0 <| s.get 0 |>.toUpper
 
+def decapitalize (s : String) :=
+  s.set 0 <| s.get 0 |>.toLower
+
 end String
 
 protected def Char.toString (c : Char) : String :=

src/Lean/Declaration.lean

@@ -186,6 +186,9 @@ structure InductiveVal extends ConstantVal where
   isReflexive : Bool
   isNested : Bool
 
+instance : Inhabited InductiveVal where
+  default := ⟨arbitrary, 0, 0, [], [], false, false, false, false⟩
+
 @[export lean_mk_inductive_val]
 def mkInductiveValEx (name : Name) (lparams : List Name) (type : Expr) (nparams nindices : Nat)
     (all ctors : List Name) (isRec isUnsafe isReflexive isNested : Bool) : InductiveVal := {

src/Lean/Parser/Command.lean

@@ -91,7 +91,7 @@ def openOnly         := parser! atomic (ident >> "(") >> many1 ident >> ")"
 def openSimple       := parser! many1 ident
 @[builtinCommandParser] def «open»    := parser! "open " >> (openHiding <|> openRenaming <|> openOnly <|> openSimple)
 
-@[builtinCommandParser] def «mutual» := parser! "mutual " >> many1 (notSymbol "end" >> commandParser) >> "end"
+@[builtinCommandParser] def «mutual» := parser! "mutual " >> many1 (ppLine >> notSymbol "end" >> commandParser) >> ppDedent (ppLine >> "end")
 @[builtinCommandParser] def «initialize» := parser! "initialize " >> optional (atomic (ident >> Term.typeSpec >> Term.leftArrow)) >> Term.doSeq
 @[builtinCommandParser] def «builtin_initialize» := parser! "builtin_initialize " >> optional (atomic (ident >> Term.typeSpec >> Term.leftArrow)) >> Term.doSeq