joint
theorem zero : True
theorem one : True
theorem two : True
by all_goals constructor
Placing the cursor at zero or one doesn't show its type in the infoview, but placing it at two does. Similarly, hovering over zero or one only shows the doc comment for the joint macro, but hovering over two shows its type.