From cd20e2ef8d30b47d8f4e838c2f63c9f69e8585c8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 11 Oct 2020 06:22:54 -0700 Subject: [PATCH] chore: use interpolated string --- src/Lean/ResolveName.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Lean/ResolveName.lean b/src/Lean/ResolveName.lean index cdd3be8ded..1c5dc2ce93 100644 --- a/src/Lean/ResolveName.lean +++ b/src/Lean/ResolveName.lean @@ -105,13 +105,13 @@ let rec loop : Name → List String → List (Name × List String) | some newId => [(newId, projs)] | none => let resolvedIds := if env.contains id then [id] else [] - let idPrv := mkPrivateName env id + let idPrv := mkPrivateName env id let resolvedIds := if env.contains idPrv then [idPrv] ++ resolvedIds else resolvedIds let resolvedIds := resolveOpenDecls env id openDecls resolvedIds let resolvedIds := getAliases env id ++ resolvedIds match resolvedIds with - | resolvedIds@(_ :: _) => resolvedIds.eraseDups.map fun id => (id, projs) - | [] => loop p (s::projs) + | _ :: _ => resolvedIds.eraseDups.map fun id => (id, projs) + | [] => loop p (s::projs) | _, _ => [] loop extractionResult.name [] @@ -189,7 +189,7 @@ variables [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m] def resolveNamespace (id : Name) : m Name := do match ResolveName.resolveNamespace? (← getEnv) (← getCurrNamespace) (← getOpenDecls) id with | some ns => return ns -| none => throwError ("unknown namespace '" ++ id ++ "'") +| none => throwError s!"unknown namespace '{id}'" /- Similar to `resolveGlobalName`, but discard any candidate whose `fieldList` is not empty. -/ def resolveGlobalConst (n : Name) : m (List Name) := do