From 4ebf1356d75684dca8367ed10e4f8d67d1630390 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 16 Sep 2020 10:14:59 -0700 Subject: [PATCH] feat: add `MetavarContext.findUserName?` --- src/Lean/MetavarContext.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index 638fc10a1d..92589e02c2 100644 --- a/src/Lean/MetavarContext.lean +++ b/src/Lean/MetavarContext.lean @@ -328,6 +328,13 @@ match mctx.decls.find? mvarId with | some decl => decl | none => panic! "unknown metavariable" +def findUserName? (mctx : MetavarContext) (userName : Name) : Option MVarId := +let search : Except MVarId Unit := mctx.decls.forM fun mvarId decl => + if decl.userName == userName then throw mvarId else pure (); +match search with +| Except.ok _ => none +| Except.error mvarId => some mvarId + def setMVarKind (mctx : MetavarContext) (mvarId : MVarId) (kind : MetavarKind) : MetavarContext := let decl := mctx.getDecl mvarId; { mctx with decls := mctx.decls.insert mvarId { decl with kind := kind } }