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

feat: add isSuffixOf

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-18 17:41:58 -08:00
parent 827e50ef1d
commit aa84adc0ea
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/Init/Lean/Data/Name.lean
View file

@ -65,6 +65,13 @@ def isPrefixOf : Name → Name → Bool
| p, n@(num p' _ _) => p == n || isPrefixOf p p'
| p, n@(str p' _ _) => p == n || isPrefixOf p p'
def isSuffixOf : Name → Name → Bool
| anonymous, _ => true
| str p₁ s₁ _, str p₂ s₂ _ => s₁ == s₂ && isSuffixOf p₁ p₂
| num p₁ n₁ _, num p₂ n₂ _ => n₁ == n₂ && isSuffixOf p₁ p₂
| _, _ => false
def lt : Name → Name → Bool
| anonymous, anonymous => false
| anonymous, _ => true