From 61c8c09c5540e6bf0a3c1aa328bdee3498cc34ed Mon Sep 17 00:00:00 2001
From: Anthony Wang <a@unnamed.website>
Date: Wed, 1 Jul 2026 03:58:17 -0400
Subject: [PATCH 1/2] Update to lean v4.30.0

---
 lean-toolchain | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lean-toolchain b/lean-toolchain
index 4c685fa..af9e5d3 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.28.0
+leanprover/lean4:v4.30.0

From ce4f3b53cf7ca4bcf583c41ed177696eaabba47a Mon Sep 17 00:00:00 2001
From: Anthony Wang <a@unnamed.website>
Date: Wed, 1 Jul 2026 04:01:20 -0400
Subject: [PATCH 2/2] Fix "Not a structure name" error for makeLenses

Previously it would fail on structures such as:

structure Blah where
  blah : Std.HashSet Nat
makeLenses Blah
---
 Lens/Elab.lean | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/Lens/Elab.lean b/Lens/Elab.lean
index 9d9c1bc..98a708d 100644
--- a/Lens/Elab.lean
+++ b/Lens/Elab.lean
@@ -21,12 +21,9 @@ elab "makeLenses" structIdent:ident : command => do
     let fieldNameIdent := mkIdent field.fieldName
     let some decl := env.find? (field.projFn)
       | throwErrorAt structIdent s!"Could not find project function {field.projFn}"
-    let (some fieldTypeName, some fieldTypeArgs) := (← liftTermElabM (liftMetaM (
-             forallTelescope decl.type fun _ body
-               => pure (body.getAppFn.constName?, body.getAppArgs.mapM (·.constName?)))))
-      | throwErrorAt structIdent "Not a structure name"
-    let d ← fieldTypeArgs.mapM fun argName => `($(mkIdent argName))
-    let fieldTypeNameIdent := Syntax.mkCApp fieldTypeName d
+    let fieldTypeNameIdent : Term ← liftTermElabM <| liftMetaM <|
+      forallTelescope decl.type fun _ body =>
+        Lean.PrettyPrinter.delab body
     let lensName := mkIdent field.fieldName
     let newVal := mkIdent <| Name.mkSimple "newVal"
     let l ←