From aa84adc0ea86eca99e06df5398a38814966104d9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 18 Jan 2020 17:41:58 -0800
Subject: [PATCH] feat: add `isSuffixOf`

---
 src/Init/Lean/Data/Name.lean | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/Init/Lean/Data/Name.lean b/src/Init/Lean/Data/Name.lean
index e1dff24002..7dcebb0220 100644
--- a/src/Init/Lean/Data/Name.lean
+++ b/src/Init/Lean/Data/Name.lean
@@ -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