chore: bump Lean to v4.23-rc2

Qpf/Macro/Common.lean

@@ -222,8 +222,6 @@ def elabCommandAndTrace (stx : Syntax)
     pure idents
 
 
-
-
 open Parser.Command in
 instance : Quote Modifiers (k := ``declModifiers) where
   quote mod :=
@@ -235,7 +233,7 @@ instance : Quote Modifiers (k := ``declModifiers) where
 
     let visibility := match mod.visibility with
       | .regular     => mkNullNode
-      | .«protected» => mkNode ``«protected» #[mkAtom "protected "]
+      | .«public» => mkNode ``«public» #[mkAtom "public "]
       | .«private»   => mkNode ``«private» #[mkAtom "private "]
 
     mkNode ``declModifiers #[

Qpf/Macro/Comp.lean

@@ -31,7 +31,6 @@ import Qq
 namespace Macro.Comp
 open MvQPF
 open Lean Elab Term Command Meta
-open Mathlib (Vector)
 
 open PrettyPrinter (delab)
 open Syntax
@@ -65,7 +64,7 @@ def synthQPF {n : Nat} (F : Q(TypeFun.{u,u} $n)) : MetaM Q(MvQPF $F) := do
   Then, tries to infer an instance of `MvQPF (TypeFun.curried F)`
 -/
 protected partial def parseApp (isLiveVar : FVarId → Bool) (F : Q(Type u)) :
-    TermElabM ((n : Nat) × Q(TypeFun.{u,u} $n) × Vector Expr n) :=
+    TermElabM ((n : Nat) × Q(TypeFun.{u,u} $n) × List.Vector Expr n) :=
   if F.isApp then
     /-
       HACK: Technically `F` is *not* an instance of `CurriedTypeFun 0`.
@@ -77,9 +76,9 @@ protected partial def parseApp (isLiveVar : FVarId → Bool) (F : Q(Type u)) :
     throwError "application expected:\n {F}"
 
 where
-  parseAppAux : {n : Nat} → Q(CurriedTypeFun.{u,u} $n) → Vector Expr n → Option Exception → _
+  parseAppAux : {n : Nat} → Q(CurriedTypeFun.{u,u} $n) → List.Vector Expr n → Option Exception → _
   | depth', Expr.app F a, args', _ => do
-    let args := Vector.cons a args'
+    let args := .cons a args'
     let depth : Nat := depth' + 1
     let F : Q(CurriedTypeFun.{u,u} $depth) := F
 
@@ -169,11 +168,11 @@ structure ElabQpfResult (u : Level) (arity : Nat) where
   qpf     : Q(@MvQPF _ $F) := by exact q(by infer_instance)
 deriving Inhabited
 
-def isLiveVar (varIds : Vector FVarId n) (id : FVarId) := varIds.toList.contains id
+def isLiveVar (varIds : List.Vector FVarId n) (id : FVarId) := varIds.toList.contains id
 
 open PrettyPrinter in
 mutual
-partial def handleLiveFVar (vars : Vector FVarId arity) (target : FVarId)  : TermElabM (ElabQpfResult u arity) := do
+partial def handleLiveFVar (vars : List.Vector FVarId arity) (target : FVarId)  : TermElabM (ElabQpfResult u arity) := do
   trace[QPF] f!"target {Expr.fvar target} is a free variable"
   let ind ← match List.indexOf' target vars.toList with
   | none      => throwError "Free variable {Expr.fvar target} is not one of the qpf arguments"
@@ -192,7 +191,7 @@ partial def handleConst (target : Q(Type u))  : TermElabM (ElabQpfResult u arity
   pure { F := const, qpf := q(Const.mvqpf)}
 
 
-partial def handleApp (vars : Vector FVarId arity) (target : Q(Type u)) : TermElabM (ElabQpfResult u arity) := do
+partial def handleApp (vars : List.Vector FVarId arity) (target : Q(Type u)) : TermElabM (ElabQpfResult u arity) := do
   let vars' := vars.toList
 
   let ⟨numArgs, F, args⟩ ← (Comp.parseApp (isLiveVar vars) target)
@@ -231,14 +230,14 @@ partial def handleApp (vars : Vector FVarId arity) (target : Q(Type u)) : TermEl
     return { F := comp, qpf }
 
 
-partial def handleArrow (binderType body : Expr) (vars : Vector FVarId arity) (targetStx : Option Term := none) (normalized := false) : TermElabM (ElabQpfResult u arity) := do
+partial def handleArrow (binderType body : Expr) (vars : List.Vector FVarId arity) (targetStx : Option Term := none) (normalized := false) : TermElabM (ElabQpfResult u arity) := do
   let newTarget ← mkAppM ``MvQPF.Arrow.Arrow #[binderType, body]
   elabQpf vars newTarget targetStx normalized
 
 /--
   Elaborate the body of a qpf
 -/
-partial def elabQpf {arity : Nat} (vars : Vector FVarId arity) (target : Q(Type u)) (targetStx : Option Term := none) (normalized := false) :
+partial def elabQpf {arity : Nat} (vars : List.Vector FVarId arity) (target : Q(Type u)) (targetStx : Option Term := none) (normalized := false) :
     TermElabM (ElabQpfResult u arity) := do
   trace[QPF] "elabQPF :: {(vars.map Expr.fvar).toList} -> {target}"
   let isLiveVar := isLiveVar vars
@@ -301,7 +300,7 @@ def elabQpfCompositionBody (view: QpfCompositionBodyView) :
     withoutAutoBoundImplicit <| do
       let target_expr ← elabTermEnsuringTypeQ (u:=u.succ.succ) view.target q(Type u)
       let arity := vars.toList.length
-      let vars : Vector _ arity := ⟨vars.toList, rfl⟩
+      let vars : List.Vector _ arity := ⟨vars.toList, rfl⟩
 
       let some vars := vars.mmap Expr.fvarId? |
         throwError "Expected all args to be fvars" -- TODO: throwErrorAt

Qpf/Macro/Data.lean

@@ -64,13 +64,8 @@ end
 open Elab.Term (TermElabM)
 
 def CtorView.declReplacePrefix (pref new_pref : Name) (ctor: CtorView) : CtorView :=
-  let declName := ctor.declName.replacePrefix pref new_pref
-  {
-    declName,
-    ref := ctor.ref
-    modifiers := ctor.modifiers
-    binders := ctor.binders
-    type? := ctor.type?
+  { ctor with
+      declName := ctor.declName.replacePrefix pref new_pref
   }
 
 
@@ -93,6 +88,16 @@ private def addSuffixToDeclIdent {m} [Monad m] [MonadResolveName m] (declId : Sy
   let (_, uncurriedDeclId, _) ← addSuffixToDeclId declId suffix
   pure ⟨uncurriedDeclId.raw[0]⟩
 
+open private elabInductiveViews from Lean.Elab.MutualInductive in
+open private elabCtors from Lean.Elab.Inductive in
+private def elabInductiveView (vars : Array Expr) (view : InductiveView) : TermElabM Unit := do
+  let view := {
+    view
+    elabCtors := fun rs r params => do
+      let ctors ← elabCtors (rs.map (·.indFVar)) params r
+      return { ctors }
+  }
+  let _ ← elabInductiveViews vars #[view]
 
 open Parser in
 /--
@@ -114,33 +119,23 @@ def mkHeadT (view : InductiveView) : CommandElabM Name := do
   -- The head type is the same as the original type, but with all constructor arguments removed
   let ctors ← view.ctors.mapM fun ctor => do
     let declName := ctor.declName.replacePrefix view.declName declName
-    pure {
+    pure { ctor with
       modifiers, declName,
-      ref := ctor.ref
-      binders := mkNullNode
+      binders := mkNullNode,
       type? := none
       : CtorView
     }
 
   -- let type ← `(Type $(mkIdent `u))
 
   -- TODO: make `HeadT` universe polymorphic
-  let view := {
+  let view := { view with
     ctors, declId, declName, shortDeclName, modifiers,
     binders         := view.binders.setArgs #[]
-    levelNames      := view.levelNames
-
-    ref             := view.ref
-    type?           := view.type?
-
-    derivingClasses := view.derivingClasses
-    computedFields  := #[]
-    : InductiveView
   }
 
   withQPFTraceNode "elabInductiveViews" <|
-    runTermElabM <| fun vars =>
-      elabInductiveViews vars #[view]
+    runTermElabM (elabInductiveView · view)
   pure declName
 
 open Parser Parser.Term Parser.Command in
@@ -267,8 +262,8 @@ def mkQpf (shapeView : InductiveView) (ctorArgs : Array CtorArgs) (headT P : Ide
       let (i, j) := (args.per_type.enum.map fun (i, t) =>
         -- the order of types is reversed, since `TypeVec`s count right-to-left
         let i := arity - 1 - i
-        ((t.indexOf? arg).map fun ⟨j, _⟩ => (i, j)).toList
-      ).toList.join.get! 0
+        ((t.idxOf? arg).map fun j => (i, j)).toList
+      ).toList.flatten[0]!
 
       `($unbox_child $(Fin2.quoteOfNat i) $(PFin2.quoteOfNat j))
 
@@ -341,15 +336,13 @@ def mkShape (view : DataView) : TermElabM MkShapeResult := do
   let modifiers : Modifiers := {
     isUnsafe := view.modifiers.isUnsafe
   }
-  let view : InductiveView := {
+  let view : InductiveView := { view with
     ctors, declId, declName, shortDeclName, modifiers, binders,
     levelNames      := []
-
-    ref             := view.ref
-    type?           := view.type?
-
-    derivingClasses := view.derivingClasses
     computedFields  := #[]
+    isClass := false
+    allowIndices := false
+    allowSortPolymorphism := false
     : InductiveView
   }
 
@@ -359,8 +352,7 @@ def mkShape (view : DataView) : TermElabM MkShapeResult := do
   return ⟨r, declName, PName, do
     withQPFTraceNode "mkShape effects" <| do
 
-    runTermElabM <| fun vars =>
-      elabInductiveViews vars #[view]
+    runTermElabM (elabInductiveView · view)
 
     let headTName ← mkHeadT view
     let childTName ← mkChildT view r headTName

Qpf/Macro/Data/Constructors.lean

@@ -49,7 +49,7 @@ def mkConstructorsWithNameAndType
       |> RecursionForm.toType retTy
 
     let modifiers : Modifiers := {
-      isNoncomputable := view.modifiers.isNoncomputable
+      computeKind := view.modifiers.computeKind
       attrs := #[{
         name := `matchPattern
       }]

Qpf/Macro/Data/Count.lean

@@ -7,10 +7,9 @@ open Lean Meta
 
 open Parser
 private partial def countVarOccurencesAux (r : Replace) (acc : Array Nat) : Syntax → Array Nat
-  | Syntax.node _ ``Term.arrow #[arg, _arrow, tail] =>     
+  | Syntax.node _ ``Term.arrow #[arg, _arrow, tail] =>
       -- NOTE: `indexOf` return an index one-past-the-end of `r.vars` if it cant find the index
-      let i := (r.vars.indexOf? arg.getId).map fun ⟨n, _⟩ => n
-      let i := i.getD acc.size
+      let i := (r.vars.idxOf? arg.getId).getD acc.size
 
       -- dbg_trace "{r.expr}.indexOf {arg} == {i}"
       -- dbg_trace "pre:  {acc}"

Qpf/Macro/Data/Replace.lean

@@ -70,12 +70,12 @@ private def ReplaceM.identFor (stx : Term) : ReplaceM m Ident := do
   let args := ctor.args.push argName
   -- dbg_trace "\nstx := {stx}\nr.expr := {r.expr}"
 
-  let name ← match r.expr.indexOf? stx with
+  let name ← match r.expr.idxOf? stx with
   | some id => do
-      let per_type := ctor.per_type.set! id $ (ctor.per_type.get! id).push argName
+      let per_type := ctor.per_type.set! id $ (ctor.per_type[id]!).push argName
       let ctor := { args, per_type }
       StateT.set { r with ctor }
-      pure $ r.vars.get! id
+      pure $ r.vars[id]!
   | none       => do
       let per_type := ctor.per_type.push #[argName]
       let name ← mkFreshBinderName

Qpf/Macro/Data/View.lean

@@ -88,6 +88,9 @@ def DataView.asInductive (view : DataView) : InductiveView
     derivingClasses := view.derivingClasses
     -- TODO: find out what these computed fields are, add support for them in `data`/`codata`
     computedFields  := #[]
+    isClass := false
+    allowIndices := false
+    allowSortPolymorphism := false
   }
 
 
@@ -259,7 +262,7 @@ def DataView.doSanityChecks (view : DataView) : CommandElabM Unit := do
 
 
 /-
-  Heavily based on `inductiveSyntaxToView` from Lean.Elab.Declaration
+  Heavily based on `inductiveSyntaxToView` from Lean.Elab.Inductive
 -/
 def dataSyntaxToView (modifiers : Modifiers) (decl : Syntax) : CommandElabM DataView :=
   withQPFTraceNode "dataSyntaxToView" (tag := "dataSyntaxToView") <| do
@@ -273,23 +276,27 @@ def dataSyntaxToView (modifiers : Modifiers) (decl : Syntax) : CommandElabM Data
   let ⟨name, declName, levelNames⟩ ← expandDeclId (← getCurrNamespace) (← getLevelNames) declId modifiers
   -- addDeclarationRanges declName decl
   let ctors      ← decl[4].getArgs.mapM fun ctor => withRef ctor do
-    -- def ctor := leading_parser optional docComment >> "\n| " >> declModifiers >> rawIdent >> optDeclSig
+    /-
+    ```
+    def ctor := leading_parser optional docComment >> "\n| " >> declModifiers >> rawIdent >> optDeclSig
+    ```
+    -/
     let mut ctorModifiers ← elabModifiers ⟨ctor[2]⟩
     if let some leadingDocComment := ctor[0].getOptional? then
       if ctorModifiers.docString?.isSome then
         logErrorAt leadingDocComment "duplicate doc string"
-      ctorModifiers := { ctorModifiers with docString? := TSyntax.getDocString ⟨leadingDocComment⟩ }
+      ctorModifiers := { ctorModifiers with docString? := some ⟨leadingDocComment⟩ }
     if ctorModifiers.isPrivate && modifiers.isPrivate then
       throwError "invalid 'private' constructor in a 'private' inductive datatype"
     if ctorModifiers.isProtected && modifiers.isPrivate then
       throwError "invalid 'protected' constructor in a 'private' inductive datatype"
     checkValidCtorModifier ctorModifiers
     let ctorName := ctor.getIdAt 3
     let ctorName := declName ++ ctorName
-    let ctorName ← withRef ctor[3] $ applyVisibility ctorModifiers.visibility ctorName
+    let ctorName ← withRef ctor[3] <| applyVisibility ctorModifiers ctorName
     let (binders, type?) := expandOptDeclSig ctor[4]
     addDocString' ctorName ctorModifiers.docString?
-    return { ref := ctor, modifiers := ctorModifiers, declName := ctorName, binders := binders, type? := type? : CtorView }
+    return { ref := ctor, declId := ctor[3], modifiers := ctorModifiers, declName := ctorName, binders := binders, type? := type? : CtorView }
   let classes ← liftCoreM <| getOptDerivingClasses decl[5]
 
 

Qpf/MathlibPort/Fin2.lean

@@ -5,6 +5,7 @@ Authors: Mario Carneiro
 -/
 
 import Mathlib.Data.Fin.Fin2
+import Mathlib.Data.Fintype.OfMap
 
 /-!
 # Inductive type variant of `Fin`

Test/DeadWrap.lean

@@ -8,7 +8,7 @@ namespace Test
 data DeadWrap (α : Type) β
   | mk : α → DeadWrap α β
 
-/-- info: 'Test.DeadWrap.Base' depends on axioms: [propext, Quot.sound] -/
+/-- info: 'Test.DeadWrap.Base' depends on axioms: [propext] -/
 #guard_msgs in
   #print axioms DeadWrap.Base