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

chore: Name.append

Browse source
This commit is contained in:
Leonardo de Moura 2022-11-29 23:04:59 -08:00
parent 733f015c65
commit dc937cb1f9
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
Lake/Util/Name.lean
View file

@ -28,9 +28,11 @@ open Lean.Name
@[simp] theorem isPrefixOf_self {n : Name} : n.isPrefixOf n := by
cases n <;> simp [isPrefixOf]
@[simp] theorem isPrefixOf_append {n m : Name} : n.isPrefixOf (n ++ m) := by
@[simp] theorem isPrefixOf_append {n m : Name} : ¬ n.hasMacroScopes → ¬ m.hasMacroScopes → n.isPrefixOf (n ++ m) := by
intro h1 h2
show n.isPrefixOf (n.append m)
induction m <;> simp [isPrefixOf, Name.append, *]
simp_all [Name.append]
clear h2; induction m <;> simp [*, Name.appendCore, isPrefixOf]
@[simp] theorem quickCmpAux_iff_eq : ∀ {n n'}, quickCmpAux n n' = .eq ↔ n = n'
| .anonymous, n => by cases n <;> simp [quickCmpAux]