The point of 'bind_len' in 'term.ml'

9 views
Skip to first unread message

Yuting Wang

unread,
Jul 24, 2018, 12:51:46 AM7/24/18
to Abella
In 'term.ml', there is a mutable variable named 'bind_len' which I think stores the length of 'bind_state'.

Since we can get the length of 'bind_state' using 'List.length'. What is the point of having 'bind_len'? 
If my understanding is correct, we should remove this variable since it causes unnecessary confusion.
Reply all
Reply to author
Forward
0 new messages