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

chore: fix comment

Browse source
This commit is contained in:
Leonardo de Moura 2020-08-10 08:39:22 -07:00
parent 43317d5598
commit e301d57b36
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/compiler/csimp.cpp
View file

@ -950,7 +950,7 @@ class csimp_fn {
let x := Array.size w in
C
```
`f z` and `Array.size w` do not share any free variable, but it `w` is an reference to a field of `w`.
`f z` and `Array.size w` do not share any free variable, but `w` is an reference to a field of `z`.
In the example above, `w` is an array, and `f z` will not be able to update the array nested there if
we have `let x := Array.size w` after it.