From ad62992373c259fb890cb2616addd188b4ea2a32 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 12 Dec 2019 08:19:13 -0800 Subject: [PATCH] feat: add `appendBefore` --- src/Init/Lean/Data/Name.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/Init/Lean/Data/Name.lean b/src/Init/Lean/Data/Name.lean index ee69ead9cb..16a91eda37 100644 --- a/src/Init/Lean/Data/Name.lean +++ b/src/Init/Lean/Data/Name.lean @@ -151,6 +151,11 @@ def appendIndexAfter : Name → Nat → Name | str p s _, idx => mkNameStr p (s ++ "_" ++ toString idx) | n, idx => mkNameStr n ("_" ++ toString idx) +def appendBefore : Name → String → Name +| anonymous, pre => mkNameStr anonymous pre +| str p s _, pre => mkNameStr p (pre ++ s) +| num p n _, pre => mkNameNum (mkNameStr p pre) n + /- The frontend does not allow user declarations to start with `_` in any of its parts. We use name parts starting with `_` internally to create auxiliary names (e.g., `_private`). -/ def isInternal : Name → Bool