syntax_data: {"ast_node_type":"other","tokens":[{"end":37,"kind":"keyword","start":0,"text":"//!"}]}
source_snippet: //! inference context when necessary.
context_before: //! goals. Visiting proof trees instead recomputes nested goals in the parents
context_after: //!