refactor: port mk_definition_inferring_unsafe to Lean (#4498)

this already can be used in two places, and will be used more as I port
more constructions. Hope the location in `Lean.Environment` is ok.

src/Lean/Environment.lean

@@ -1060,4 +1060,11 @@ instance (m n) [MonadLift m n] [MonadEnv m] : MonadEnv n where
   getEnv    := liftM (getEnv : m Environment)
   modifyEnv := fun f => liftM (modifyEnv f : m Unit)
 
+/-- Constructs a DefinitionVal, inferring the `unsafe` field -/
+def mkDefinitionValInferrringUnsafe [Monad m] [MonadEnv m] (name : Name) (levelParams : List Name)
+    (type : Expr) (value : Expr) (hints : ReducibilityHints) : m DefinitionVal := do
+  let env ← getEnv
+  let safety := if env.hasUnsafe type || env.hasUnsafe value then DefinitionSafety.unsafe else DefinitionSafety.safe
+  return { name, levelParams, type, value, hints, safety }
+
 end Lean

src/Lean/Meta/Closure.lean

@@ -349,14 +349,9 @@ end Closure
 def mkAuxDefinition (name : Name) (type : Expr) (value : Expr) (zetaDelta : Bool := false) (compile : Bool := true) : MetaM Expr := do
   let result ← Closure.mkValueTypeClosure type value zetaDelta
   let env ← getEnv
-  let decl := Declaration.defnDecl {
-    name        := name
-    levelParams := result.levelParams.toList
-    type        := result.type
-    value       := result.value
-    hints       := ReducibilityHints.regular (getMaxHeight env result.value + 1)
-    safety      := if env.hasUnsafe result.type || env.hasUnsafe result.value then DefinitionSafety.unsafe else DefinitionSafety.safe
-  }
+  let hints := ReducibilityHints.regular (getMaxHeight env result.value + 1)
+  let decl := Declaration.defnDecl (← mkDefinitionValInferrringUnsafe name result.levelParams.toList
+    result.type result.value  hints)
   addDecl decl
   if compile then
     compileDecl decl

src/Lean/Meta/Match/Match.lean

@@ -776,14 +776,8 @@ def mkMatcherAuxDefinition (name : Name) (type : Expr) (value : Expr) : MetaM (E
   match (matcherExt.getState env).find? (result.value, compile) with
   | some nameNew => return (mkMatcherConst nameNew, none)
   | none =>
-    let decl := Declaration.defnDecl {
-      name
-      levelParams := result.levelParams.toList
-      type        := result.type
-      value       := result.value
-      hints       := ReducibilityHints.abbrev
-      safety      := if env.hasUnsafe result.type || env.hasUnsafe result.value then DefinitionSafety.unsafe else DefinitionSafety.safe
-    }
+    let decl := Declaration.defnDecl (← mkDefinitionValInferrringUnsafe name result.levelParams.toList
+      result.type result.value .abbrev)
     trace[Meta.Match.debug] "{name} : {result.type} := {result.value}"
     let addMatcher : MatcherInfo → MetaM Unit := fun mi => do
       addDecl decl