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

chore: naming convention

Browse source
This commit is contained in:
Leonardo de Moura 2021-05-01 21:29:06 -07:00
parent 93189e0fce
commit 663a5124f4
2 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/LocalContext.lean
View file

@ -254,7 +254,7 @@ def numIndices (lctx : LocalContext) : Nat :=
lctx.decls.size
@[export lean_local_ctx_get]
def getAt! (lctx : LocalContext) (i : Nat) : Option LocalDecl :=
def getAt? (lctx : LocalContext) (i : Nat) : Option LocalDecl :=
lctx.decls.get! i
section

6
src/Lean/Meta/ExprDefEq.lean
View file

@ -289,7 +289,7 @@ where
let start := lctx.getFVar! xs[0] |>.index
let stop := lctx.getFVar! xs.back |>.index
for i in [start+1:stop] do
match lctx.getAt! i with
match lctx.getAt? i with
| some localDecl =>
if localDecl.isLet then
return true
@ -331,7 +331,7 @@ where
if i+1 == (← read) then
return ()
else
match (← getLCtx).getAt! (i+1) with
match (← getLCtx).getAt? (i+1) with
| none => collectLetDepsAux i
| some localDecl =>
if (← get).contains localDecl.fvarId then
@ -360,7 +360,7 @@ where
let stop := lctx.getFVar! xs.back |>.index
let mut ys := #[]
for i in [start:stop+1] do
match lctx.getAt! i with
match lctx.getAt? i with
| none => pure ()
| some localDecl =>
if s.contains localDecl.fvarId then