From bd7e6c3c6125085a2016ce476ece60c08781e1da Mon Sep 17 00:00:00 2001 From: Cameron Zwarich Date: Sun, 6 Jul 2025 05:58:13 -0700 Subject: [PATCH] chore: use ``-prefixed Names when possible (#9217) --- src/Lean/Compiler/LCNF/ElimDeadBranches.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Lean/Compiler/LCNF/ElimDeadBranches.lean b/src/Lean/Compiler/LCNF/ElimDeadBranches.lean index 3a161abce7..80a4be3bca 100644 --- a/src/Lean/Compiler/LCNF/ElimDeadBranches.lean +++ b/src/Lean/Compiler/LCNF/ElimDeadBranches.lean @@ -209,10 +209,10 @@ partial def getLiteral (v : Value) : CompilerM (Option ((Array CodeDecl) × FVar return none where go : Value → CompilerM ((Array CodeDecl) × FVarId) - | .ctor `Nat.zero #[] .. => do + | .ctor ``Nat.zero #[] .. => do let decl ← mkAuxLetDecl <| .lit <| .nat <| 0 return (#[.let decl], decl.fvarId) - | .ctor `Nat.succ #[val] .. => do + | .ctor ``Nat.succ #[val] .. => do let val := getNatConstant val + 1 let decl ← mkAuxLetDecl <| .lit <| .nat <| val return (#[.let decl], decl.fvarId) @@ -228,8 +228,8 @@ where | _ => unreachable! getNatConstant : Value → Nat - | .ctor `Nat.zero #[] .. => 0 - | .ctor `Nat.succ #[val] .. => getNatConstant val + 1 + | .ctor ``Nat.zero #[] .. => 0 + | .ctor ``Nat.succ #[val] .. => getNatConstant val + 1 | _ => panic! "Not a well formed Nat constant Value" end Value