From c8f448ecd3ccb691c133c529fa17d4ff7cdf10ed Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 24 Jul 2020 11:50:44 -0700 Subject: [PATCH] feat: add `updateBinderInfo` --- src/Lean/LocalContext.lean | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/Lean/LocalContext.lean b/src/Lean/LocalContext.lean index 34e4f30919..c634bcb296 100644 --- a/src/Lean/LocalContext.lean +++ b/src/Lean/LocalContext.lean @@ -63,6 +63,10 @@ def updateUserName : LocalDecl → Name → LocalDecl | cdecl index id _ type bi, userName => cdecl index id userName type bi | ldecl index id _ type val, userName => ldecl index id userName type val +def updateBinderInfo : LocalDecl → BinderInfo → LocalDecl +| cdecl index id n type _, bi => cdecl index id n type bi +| ldecl _ _ _ _ _, _ => panic! "unexpected let declaration" + def toExpr (decl : LocalDecl) : Expr := mkFVar decl.fvarId @@ -203,6 +207,16 @@ match lctx with { fvarIdToDecl := map.insert decl.fvarId decl, decls := decls.set decl.index decl } +def updateBinderInfo (lctx : LocalContext) (fvarId : FVarId) (bi : BinderInfo) : LocalContext := +match lctx with +| { fvarIdToDecl := map, decls := decls } => + match lctx.find? fvarId with + | none => lctx + | some decl => + let decl := decl.updateBinderInfo bi; + { fvarIdToDecl := map.insert decl.fvarId decl, + decls := decls.set decl.index decl } + @[export lean_local_ctx_num_indices] def numIndices (lctx : LocalContext) : Nat := lctx.decls.size