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

chore: improve sanitizeNames superscripts

Browse source 
cc @Kha
This commit is contained in:
Leonardo de Moura 2020-09-17 08:57:54 -07:00
parent 71f91cca23
commit e9d65dd2de
3 changed files with 16 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/Lean/LocalContext.lean
View file

@ -373,7 +373,10 @@ Id.run $ lctx.allM p
private def mkInaccessibleUserNameAux (unicode : Bool) (name : Name) (idx : Nat) : Name :=
if unicode then
name.appendAfter ("✝" ++ idx.toSuperscriptString)
if idx == 0 then
name.appendAfter "✝"
else
name.appendAfter ("✝" ++ idx.toSuperscriptString)
else
name ++ mkNameNum "_inaccessible" idx
@ -420,7 +423,7 @@ let (lctx, _, _) := lctx.decls.size.foldRev
let userName := decl.userName;
if userName.hasMacroScopes || usedNames.contains userName then
let userName := userName.eraseMacroScopes;
let idx := (usedName2Idx.find? userName).getD 1;
let idx := (usedName2Idx.find? userName).getD 0;
let (userNameNew, usedName2Idx) := mkFreshInaccessibleUserName unicode usedName2Idx userName idx;
let lctx := lctx.setUserName decl.fvarId userNameNew;
(lctx, usedNames, usedName2Idx)

2
tests/lean/shadow.lean
View file

@ -16,5 +16,5 @@ set_option pp.sanitizeNames false in
def foo2 {α} [Inhabited α] (inst inst : α) : {β δ : Type} → α → β → δ → α × β × δ :=
_
def foo3 {α β} (inst : α) (b : β) (inst : α) [Inhabited α] : {β δ : Type} → α → β → δ → α × β × δ :=
def foo3 {α β} (inst : α) (inst : β) (b : β) (inst : α) [Inhabited α] : {β δ : Type} → α → β → δ → α × β × δ :=
_

20
tests/lean/shadow.lean.expected.out
View file

@ -1,11 +1,11 @@
shadow.lean:6:0: error: type mismatch
h
has type
x✝¹ = x✝¹
x✝ = x✝
but it is expected to have type
x = x
failed to synthesize instance
CoeT (x✝¹ = x✝¹) h (x = x)
CoeT (x✝ = x✝) h (x = x)
shadow.lean:10:0: error: type mismatch
h
has type
@ -17,10 +17,10 @@ failed to synthesize instance
shadow.lean:13:0: error: don't know how to synthesize placeholder
context:
α : Type u_1
inst✝² : Inhabited α
inst✝¹ inst : α
β✝¹ δ✝¹ : Type
⊢ α → β✝¹ → δ✝¹ → α × β✝¹ × δ✝¹
inst✝¹ : Inhabited α
inst✝ inst : α
β✝ δ✝ : Type
⊢ α → β✝ → δ✝ → α × β✝ × δ✝
shadow.lean:17:0: error: don't know how to synthesize placeholder
context:
α : Type u_1
@ -33,8 +33,8 @@ context:
α : Type u_1
β : Sort u_2
inst✝² : α
b : β
inst✝¹ b : β
inst : α
inst✝¹ : Inhabited α
β✝¹ δ✝¹ : Type
⊢ α → β✝¹ → δ✝¹ → α × β✝¹ × δ✝¹
inst✝ : Inhabited α
β✝ δ✝ : Type
⊢ α → β✝ → δ✝ → α × β✝ × δ✝