From d6a3e22992c1048eb4ec0cba6f35b4fb2e69077d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 13 Sep 2020 13:13:34 -0700
Subject: [PATCH] chore: add auxiliary function

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

diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean
index e7e2c18382..c40830b05f 100644
--- a/src/Lean/MetavarContext.lean
+++ b/src/Lean/MetavarContext.lean
@@ -1090,6 +1090,9 @@ let (e, s) := LevelMVarToParam.main e { paramNamePrefix := paramNamePrefix, alre
   nextParamIdx  := s.nextParamIdx,
   expr          := e }
 
+def getExprAssignmentDomain (mctx : MetavarContext) : Array MVarId :=
+mctx.eAssignment.foldl (fun a mvarId _ => Array.push a mvarId) #[]
+
 end MetavarContext
 
 class MonadMCtx (m : Type → Type) :=