feat(frontends): local names in user-defined notation#701

b-mehta wants to merge 1 commit into

masterleanprover-community/lean:masterfrom

b-mehta-patch-1leanprover-community/lean:b-mehta-patch-1Copy head branch name to clipboard