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

feat: add MetavarContext.findUserName?

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-16 10:14:59 -07:00
parent d00dc1988a
commit 4ebf1356d7
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/Lean/MetavarContext.lean
View file

@ -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 } }