From ad53983e35cf80580efe9cc1fac81ae47b0fbd08 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 3 Aug 2020 11:35:58 -0700
Subject: [PATCH] feat: add `FVarSubst.domain`

---
 src/Lean/Meta/Tactic/FVarSubst.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Lean/Meta/Tactic/FVarSubst.lean b/src/Lean/Meta/Tactic/FVarSubst.lean
index b4ae3c519e..29a4872a65 100644
--- a/src/Lean/Meta/Tactic/FVarSubst.lean
+++ b/src/Lean/Meta/Tactic/FVarSubst.lean
@@ -63,6 +63,9 @@ else oldS.map.fold
       | some fvarId'' => m.insert fvarId fvarId'')
   newS
 
+def domain (s : FVarSubst) : List FVarId :=
+s.map.fold (fun r k v => k :: r) []
+
 end FVarSubst
 end Meta