diff --git a/Qpf/Macro/Common.lean b/Qpf/Macro/Common.lean
index 7fe7c16..538df0c 100644
--- a/Qpf/Macro/Common.lean
+++ b/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 #[
diff --git a/Qpf/Macro/Comp.lean b/Qpf/Macro/Comp.lean
index 517befa..134d424 100644
--- a/Qpf/Macro/Comp.lean
+++ b/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
diff --git a/Qpf/Macro/Data.lean b/Qpf/Macro/Data.lean
index 36d48f2..575306c 100644
--- a/Qpf/Macro/Data.lean
+++ b/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,10 +119,9 @@ 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
     }
@@ -125,22 +129,13 @@ def mkHeadT (view : InductiveView) : CommandElabM Name := do
   -- 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
diff --git a/Qpf/Macro/Data/Constructors.lean b/Qpf/Macro/Data/Constructors.lean
index a45e249..2c9dce5 100644
--- a/Qpf/Macro/Data/Constructors.lean
+++ b/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
       }]
diff --git a/Qpf/Macro/Data/Count.lean b/Qpf/Macro/Data/Count.lean
index 17df217..8899b80 100644
--- a/Qpf/Macro/Data/Count.lean
+++ b/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}"
diff --git a/Qpf/Macro/Data/Replace.lean b/Qpf/Macro/Data/Replace.lean
index c868252..e2bd69e 100644
--- a/Qpf/Macro/Data/Replace.lean
+++ b/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
diff --git a/Qpf/Macro/Data/View.lean b/Qpf/Macro/Data/View.lean
index 9d756db..a08102d 100644
--- a/Qpf/Macro/Data/View.lean
+++ b/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,12 +276,16 @@ 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
@@ -286,10 +293,10 @@ def dataSyntaxToView (modifiers : Modifiers) (decl : Syntax) : CommandElabM Data
     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]
 
 
diff --git a/Qpf/MathlibPort/Fin2.lean b/Qpf/MathlibPort/Fin2.lean
index 0bbaea9..2cd1828 100644
--- a/Qpf/MathlibPort/Fin2.lean
+++ b/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`
diff --git a/Test/DeadWrap.lean b/Test/DeadWrap.lean
index 7c0ce5d..09cdf7f 100644
--- a/Test/DeadWrap.lean
+++ b/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
 
diff --git a/lake-manifest.json b/lake-manifest.json
index 276669f..1a7c33f 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,17 +5,17 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "4bbdccd9c5f862bf90ff12f0a9e2c8be032b9a84",
+   "rev": "595c2c615b545c3421ac5f8b568efee290e73962",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.14.0",
+   "inputRev": "master",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa",
+   "rev": "240eddc1bb31420fbbc57fe5cc579435c2522493",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b",
+   "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,57 +35,57 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "519e509a28864af5bed98033dd33b95cf08e9aa7",
+   "rev": "dba7fbc707774d1ba830fd44d7f92a717e9bf57f",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.14.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "68280daef58803f68368eb2e53046dabcd270c9d",
+   "rev": "6e47cc88cfbf1601ab364e9a4de5f33f13401ff8",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.47",
+   "inputRev": "v0.0.71",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5a0ec8588855265ade536f35bcdcf0fb24fd6030",
+   "rev": "523c8ee53f7057447fc62ec14e506fda4cf63dfa",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.14.0",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41",
+   "rev": "f85ad59c9b60647ef736719c23edd4578f723806",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8d6c853f11a5172efa0e96b9f2be1a83d861cdd9",
+   "rev": "6e89c7370ca3a91b7d1f29ef7d727a9d027d7b0d",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.14.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d",
+   "rev": "cacb481a1eaa4d7d4530a27b606c60923da21caf",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lakefile.lean b/lakefile.lean
index bbc6456..375695b 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -12,4 +12,4 @@ lean_lib Test
 lean_lib ITree
 
 require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git"@"v4.14.0"
+  "https://github.com/leanprover-community/mathlib4.git"@"master"
diff --git a/lean-toolchain b/lean-toolchain
index 401bc14..27770b5 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.14.0
\ No newline at end of file
+leanprover/lean4:v4.23.0-rc2
\ No newline at end of file