You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.