chore: bump toolchain to v4.14.0 (#59)

Qpf/Macro/Data.lean

@@ -139,7 +139,8 @@ def mkHeadT (view : InductiveView) : CommandElabM Name := do
   }
 
   withQPFTraceNode "elabInductiveViews" <|
-    elabInductiveViews #[view]
+    runTermElabM <| fun vars =>
+      elabInductiveViews vars #[view]
   pure declName
 
 open Parser Parser.Term Parser.Command in
@@ -358,7 +359,8 @@ def mkShape (view : DataView) : TermElabM MkShapeResult := do
   return ⟨r, declName, PName, do
     withQPFTraceNode "mkShape effects" <| do
 
-    elabInductiveViews #[view]
+    runTermElabM <| fun vars =>
+      elabInductiveViews vars #[view]
 
     let headTName ← mkHeadT view
     let childTName ← mkChildT view r headTName
@@ -444,7 +446,7 @@ open Macro Comp in
 def elabData : CommandElab := fun stx =>
   withQPFTraceNode "elabData" (tag := "elabData") (collapsed := false) <| do
 
-  let modifiers ← elabModifiers stx[0]
+  let modifiers ← elabModifiers ⟨stx[0]⟩
   let decl := stx[1]
 
   let view ← dataSyntaxToView modifiers decl

Qpf/Macro/Data/View.lean

@@ -270,11 +270,11 @@ def dataSyntaxToView (modifiers : Modifiers) (decl : Syntax) : CommandElabM Data
   let (binders, type?) := expandOptDeclSig decl[2]
 
   let declId  : TSyntax ``declId := ⟨decl[1]⟩
-  let ⟨name, declName, levelNames⟩ ← expandDeclId declId modifiers
-  addDeclarationRanges declName decl
+  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
-    let mut ctorModifiers ← elabModifiers ctor[2]
+    let mut ctorModifiers ← elabModifiers ⟨ctor[2]⟩
     if let some leadingDocComment := ctor[0].getOptional? then
       if ctorModifiers.docString?.isSome then
         logErrorAt leadingDocComment "duplicate doc string"
@@ -289,7 +289,6 @@ def dataSyntaxToView (modifiers : Modifiers) (decl : Syntax) : CommandElabM Data
     let ctorName ← withRef ctor[3] $ applyVisibility ctorModifiers.visibility ctorName
     let (binders, type?) := expandOptDeclSig ctor[4]
     addDocString' ctorName ctorModifiers.docString?
-    addAuxDeclarationRanges ctorName ctor ctor[3]
     return { ref := ctor, modifiers := ctorModifiers, declName := ctorName, binders := binders, type? := type? : CtorView }
   let classes ← liftCoreM <| getOptDerivingClasses decl[5]
 

Qpf/MathlibPort/Fin2.lean

@@ -92,9 +92,9 @@ instance IsLt.succ m n [l : IsLt m n] : IsLt (succ m) (succ n) :=
 /-- Use type class inference to infer the boundedness proof, so that we can directly convert a
 `nat` into a `PFin2 n`. This supports notation like `&1 : fin 3`. -/
 def ofNat' : ∀ {n} m [IsLt m n], PFin2 n
-  | 0, _, ⟨h⟩ => absurd h (Nat.not_lt_zero _)
-  | succ _, 0, ⟨_⟩ => fz
-  | succ n, succ m, ⟨h⟩ => fs (@ofNat' n m ⟨lt_of_succ_lt_succ h⟩)
+  | 0, _, i => absurd i.h (Nat.not_lt_zero _)
+  | succ _, 0, _ => fz
+  | succ n, succ m, i => fs (@ofNat' n m ⟨lt_of_succ_lt_succ i.h⟩)
 
 instance : Inhabited (PFin2 1) :=
   ⟨fz⟩

Qpf/PFunctor/Multivariate/Constructions/Sum.lean

@@ -12,29 +12,25 @@ namespace Sum
 
 universe u
 
-def SumPFunctor : MvPFunctor.{u} 2
-  := ⟨PFin2 2,
-      fun
-      | 0 => !![PFin2 1, PFin2 0] -- inl
-      | 1 => !![PFin2 0, PFin2 1] -- inr
-    ⟩
-
+def SumPFunctor : MvPFunctor.{u} 2 :=
+  ⟨PFin2 2, fun
+    | 0 => !![PFin2 1, PFin2 0] -- inl
+    | 1 => !![PFin2 0, PFin2 1] -- inr
+  ⟩
 
 abbrev QpfSum' := SumPFunctor.Obj
 abbrev QpfSum  := TypeFun.curried QpfSum'
 
-def inl {Γ : TypeVec 2} (a : Γ 1) : QpfSum' Γ
-  := ⟨PFin2.ofNat' 0,
-      fun
-      | 1, _ => a
-    ⟩
-
-def inr {Γ : TypeVec 2} (b : Γ 0) : QpfSum' Γ
-  := ⟨PFin2.ofNat' 1,
-      fun
-      | 0, _ => b
-      | 1, x => by cases x
-    ⟩
+def inl {Γ : TypeVec 2} (a : Γ 1) : QpfSum' Γ :=
+  ⟨PFin2.ofNat' 0, fun
+    | 1, _ => a
+  ⟩
+
+def inr {Γ : TypeVec 2} (b : Γ 0) : QpfSum' Γ :=
+  ⟨PFin2.ofNat' 1, fun
+    | 0, _ => b
+    | 1, (x : PFin2 _) => by cases x
+  ⟩
 
 
 def Sum' := @TypeFun.ofCurried 2 Sum