Skip to content
Norbert Preining edited this page Oct 6, 2017 · 2 revisions

parse [ in <mod-exp> : ] <term> .

Tries to parse the given term within the module specified by the module expression <mod-exp>, or the current module if not given, and returns the parsed and qualified term.

In case of ambiguous terms, i.e., different possible parse trees, the command will prompt for one of the trees.

Related: qualified term

Clone this wiki locally