From d0203ca1dc27a2ccd4015b1382f255029bbf45b1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 15 Aug 2022 13:03:07 -0700 Subject: [PATCH] feat: add `Decl.ensureUniqueLetVarNames` --- src/Lean/Compiler/Decl.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/Lean/Compiler/Decl.lean b/src/Lean/Compiler/Decl.lean index 87d186d61b..9794c7eb85 100644 --- a/src/Lean/Compiler/Decl.lean +++ b/src/Lean/Compiler/Decl.lean @@ -115,4 +115,12 @@ def Decl.toString (decl : Decl) : CoreM String := do Meta.MetaM.run' do return s!"{decl.name} : {← Meta.ppExpr decl.type} :=\n{← Meta.ppExpr decl.value}" +/-- +Make sure all let-declarations have unique user-facing names. + +See `Compiler.ensureUniqueLetVarNames` +-/ +def Decl.ensureUniqueLetVarNames (decl : Decl) : CoreM Decl := do + return { decl with value := (← Compiler.ensureUniqueLetVarNames decl.value) } + end Lean.Compiler