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

feat: extend set of valid characters that can occur in an auto bound implicit local name suffix

Browse source
This commit is contained in:
Leonardo de Moura 2021-02-02 10:29:29 -08:00
parent 729047b5a2
commit bda39b9a72
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/Elab/AutoBound.lean
View file

@ -14,8 +14,8 @@ register_builtin_option autoBoundImplicitLocal : Bool := {
descr := "Unbound local variables in declaration headers become implicit arguments if they are a lower case or greek letter followed by numeric digits. For example, `def f (x : Vector α n) : Vector α n :=` automatically introduces the implicit variables {α n}."
}
private def allNumeral (s : Substring) : Bool :=
s.all fun c => c.isDigit || isNumericSubscript c
private def isValidAutoBoundSuffix (s : String) : Bool :=
s.toSubstring.drop 1 |>.all fun c => c.isDigit || isSubScriptAlnum c || c == '_' || c == '\''
/-
Remark: Issue #255 exposed a nasty interaction between macro scopes and auto-bound-implicit names.
@ -33,12 +33,12 @@ Therefore, we do consider identifier with macro scopes anymore.
def isValidAutoBoundImplicitName (n : Name) : Bool :=
match n with
| Name.str Name.anonymous s _ => s.length > 0 && (isGreek s[0] || s[0].isLower) && allNumeral (s.toSubstring.drop 1)
| Name.str Name.anonymous s _ => s.length > 0 && (isGreek s[0] || s[0].isLower) && isValidAutoBoundSuffix s
| _ => false
def isValidAutoBoundLevelName (n : Name) : Bool :=
match n with
| Name.str Name.anonymous s _ => s.length > 0 && s[0].isLower && allNumeral (s.toSubstring.drop 1)
| Name.str Name.anonymous s _ => s.length > 0 && s[0].isLower && isValidAutoBoundSuffix s
| _ => false
end Lean.Elab