feat: mark auxiliary eliminators as [inline]

src/Lean/Compiler/InlineAttrs.lean

@@ -62,5 +62,8 @@ hasInlineAttrAux env InlineAttributeKind.noinline n
 def hasMacroInlineAttribute (env : Environment) (n : Name) : Bool :=
 hasInlineAttrAux env InlineAttributeKind.macroInline n
 
+def setInlineAttribute (env : Environment) (declName : Name) (kind : InlineAttributeKind) : Except String Environment :=
+inlineAttrs.setValue env declName kind
+
 end Compiler
 end Lean

src/Lean/Meta/Basic.lean

@@ -10,6 +10,7 @@ import Lean.ReducibilityAttrs
 import Lean.Util.Trace
 import Lean.Util.RecDepth
 import Lean.Util.Closure
+import Lean.Compiler.InlineAttrs
 import Lean.Meta.Exception
 import Lean.Meta.DiscrTreeTypes
 import Lean.Eval
@@ -259,6 +260,11 @@ ctx ← read;
 s ← get;
 throw (Exception.other ref (MessageData.withContext { env := s.env, mctx := s.mctx, lctx := ctx.lctx, opts := ctx.config.opts } msg))
 
+@[inline] def ofExcept {α ε} [HasToString ε] (x : Except ε α) : MetaM α :=
+match x with
+| Except.ok a    => pure a
+| Except.error e => throwOther (toString e)
+
 def throwBug {α} (b : Bug) : MetaM α :=
 throwEx $ Exception.bug b
 
@@ -860,6 +866,12 @@ type ← inferType value;
 let type := type.headBeta;
 mkAuxDefinition name type value
 
+def setInlineAttribute (declName : Name) (kind := Compiler.InlineAttributeKind.inline): MetaM Unit := do
+env ← getEnv;
+match Compiler.setInlineAttribute env declName kind with
+| Except.ok env    => setEnv env
+| Except.error msg => throwOther msg
+
 private partial def instantiateForallAux (ps : Array Expr) : Nat → Expr → MetaM Expr
 | i, e =>
   if h : i < ps.size then do

src/Lean/Meta/EqnCompiler/DepElim.lean

@@ -732,6 +732,7 @@ generalizeTelescope majors.toArray `_d fun majors => do
     val  ← mkLambda args mvar;
     trace! `Meta.EqnCompiler.matchDebug ("eliminator value: " ++ val ++ "\ntype: " ++ type);
     elim ← mkAuxDefinition elimName type val;
+    setInlineAttribute elimName;
     trace! `Meta.EqnCompiler.matchDebug ("eliminator: " ++ elim);
     let unusedAltIdxs : List Nat := lhss.length.fold
       (fun i r => if s.used.contains i then r else i::r)