chore: update std 12-05 (#863)

Co-authored-by: Gabriel Ebner <gebner@gebner.org>

Author: digama0

Mathlib/Lean/Expr/Basic.lean

@@ -6,6 +6,7 @@ Floris van Doorn, E.W.Ayers, Arthur Paulino
 -/
 import Lean
 import Mathlib.Util.MapsTo
+import Std.Lean.Expr
 import Std.Data.List.Basic
 
 /-!
@@ -264,14 +265,6 @@ def addLocalVarInfoForBinderIdent (fvar : Expr) : TSyntax ``binderIdent → Term
 | `(binderIdent| $n:ident) => Elab.Term.addLocalVarInfo n fvar
 | tk => Elab.Term.addLocalVarInfo (Unhygienic.run `(_%$tk)) fvar
 
-/-- Converts an `Expr` into a `Syntax`, by creating a fresh metavariable
-assigned to the expr and  returning a named metavariable syntax `?a`. -/
-def toSyntax (e : Expr) : TermElabM Syntax.Term := withFreshMacroScope do
-  let stx ← `(?a)
-  let mvar ← elabTermEnsuringType stx (← Meta.inferType e)
-  mvar.mvarId!.assign e
-  pure stx
-
 end Expr
 
 end Lean

Mathlib/Order/Basic.lean

@@ -655,7 +655,7 @@ variable [Preorder α] [Nonempty β] {a b : α}
 
 @[simp] lemma const_le_const : const β a ≤ const β b ↔ a ≤ b := by simp [Pi.le_def]
 @[simp] lemma const_lt_const : const β a < const β b ↔ a < b := by
-  simpa [Pi.lt_def] using le_of_lt (α := _)
+  simpa [Pi.lt_def] using le_of_lt (α := α)
 
 end Function
 

lake-manifest.json

@@ -34,7 +34,7 @@
   {"git":
    {"url": "https://github.com/JLimperg/aesop",
     "subDir?": null,
-    "rev": "70c59fcfc63de90786d59222c32468dab87964c5",
+    "rev": "61004154b4a8f7aec6224745f4fbddeda5795e97",
     "name": "aesop",
     "inputRev?": "master"}},
   {"git":
@@ -52,6 +52,6 @@
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "42bb39d34ec7dcb07580458efa4a7936bd5192b7",
+    "rev": "cad19f171ad4aebe091e6deeb9a43a14521bfbfe",
     "name": "std",
     "inputRev?": "main"}}]}