feat: preserve variable names when packing domain

2021-12-17 07:10:26 -08:00 · 2021-12-17 07:10:26 -08:00 · 6b82e15069
commit 6b82e15069
parent 8b7411bdd8
2 changed files with 5 additions and 3 deletions
--- a/src/Lean/Elab/PreDefinition/WF/PackDomain.lean
+++ b/src/Lean/Elab/PreDefinition/WF/PackDomain.lean
@ -43,7 +43,9 @@ private partial def mkPSigmaCasesOn (y : Expr) (codomain : Expr) (xs : Array Exp
  let mvar ← mkFreshExprSyntheticOpaqueMVar codomain
  let rec go (mvarId : MVarId) (y : FVarId) (ys : Array Expr) : MetaM Unit := do
    if ys.size < xs.size - 1 then
-      let #[s] ← cases mvarId y | unreachable!
+      let xDecl  ← getLocalDecl xs[ys.size].fvarId!
+      let xDecl' ← getLocalDecl xs[ys.size + 1].fvarId!
+      let #[s] ← cases mvarId y #[{ varNames := [xDecl.userName, xDecl'.userName] }] | unreachable!
      go s.mvarId s.fields[1].fvarId! (ys.push s.fields[0])
    else
      let ys := ys.push (mkFVar y)
--- a/tests/lean/wf2.lean.expected.out
+++ b/tests/lean/wf2.lean.expected.out
@ -1,3 +1,3 @@
 wf2.lean:3:8-3:17: error: unsolved goals
-fst✝ snd✝ : Nat
-⊢ fst✝ - 1 < fst✝
+x y : Nat
+⊢ x - 1 < x