#28 "Type of" buttom

[Leo Freitas]

It is often important to know the types, in particular of schema signatures, during proofs. It would be nice to be able to show the type of a selected expression within the goal. And it should be easy to either typecheck on the fly or get the name involved and check it against the section manager.

Similarly, it would be nice to have a "type of" button or squigle to know the type of certain paragraph. There is a tooltip with the type somehow already but copying is awkward. :-(