HOL icon indicating copy to clipboard operation
HOL copied to clipboard

Add tooltip type information to record fields

Open mn200 opened this issue 5 years ago • 0 comments

It's clearly useful to be able to see exactly what term is hiding underneath the fld of something like r.fld.

mn200 avatar Sep 18 '18 00:09 mn200