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

feat: add updateBinderInfo

Browse source
This commit is contained in:
Leonardo de Moura 2020-07-24 11:50:44 -07:00
parent 0bbaf161be
commit c8f448ecd3
1 changed files with 14 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/Lean/LocalContext.lean
View file

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