- [[exact-show]] : Include the `term : type` information when closing a goal. The [[exact-tactic|exact]] tactic specifies the `hypotheses`term that witnesses of the `goal`type., but the reader is required to glance back and forth to read the goal type in the infoview. To reduce scanning back and forth to the infoview, the exact-show idiom provides information equivalent to the term : type definition. exact `<Goal>` show from `<Hypotheses>`, where the `Hypotheses` term is a witness of the `Goal` type.