max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: use interpolated string

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-11 06:22:54 -07:00
parent adc33da468
commit cd20e2ef8d
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Lean/ResolveName.lean
View file

@ -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