HOL
HOL copied to clipboard
Add tooltip type information to record fields
It's clearly useful to be able to see exactly what term is hiding underneath the fld
of something like r.fld
.
It's clearly useful to be able to see exactly what term is hiding underneath the fld
of something like r.fld
.