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

style: statement ordering

Browse source 
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
This commit is contained in:
Wojciech Nawrocki 2021-07-30 10:30:37 -07:00 • committed by Sebastian Ullrich
parent 0b6d51d60b
commit 5f021baa95
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Server/FileWorker/Utils.lean
View file

@ -76,8 +76,8 @@ def store (st : RpcSessionState) (typeName : Name) (obj : NonScalar) : Lsp.RpcRe
(ref, st')
def release (st : RpcSessionState) (ref : Lsp.RpcRef) : Bool × RpcSessionState :=
let st' := { st with aliveRefs := st.aliveRefs.erase ref }
(st.aliveRefs.contains ref, st')
let released := st.aliveRefs.contains ref
(released, { st with aliveRefs := st.aliveRefs.erase ref })
end RpcSessionState