User-defined notation parsers #1617
Conversation
|
I fear I might give @leodemoura a heart attack with this commit, but I hope the results justify the means :) . |
Kha
force-pushed
the
user-notation
branch
5 times, most recently
from
3d5bf94 to
f69fd6a
Compare
library/init/meta/interactive.lean
Outdated
| @@ -133,813 +132,3 @@ meta def param_desc : expr → tactic format | |||
| then return $ to_fmt "{ tactic }" | |||
| else paren <$> pp e | |||
| end interactive | |||
|
|
|||
There was a problem hiding this comment.
Is everyone fine with this refactoring to reduce dependencies? If yes, I'd recommend merging the PR as-is to reduce merge conflicts. I will improve error handling in a later PR.
There was a problem hiding this comment.
I am fine with reducing dependencies, but a new directory tactic with a single interactive.lean file looks strange. I think interactive_base.lean and interactive.lean in the same directory (i.e., meta) looks better.
BTW, I'm not against mirroring the namespace hierarchy in the directory structure. However, if you do it, we should be consistent. We should also do it in a different PR. What do you think?
There was a problem hiding this comment.
We could move the *_tactic(s).lean files into the directory. However, your suggestion is probably better for the time being since it avoids conflicts with other open PRs. I will do the change.
… to implement interpolating format macro
…and start putting them to use
Kha
changed the title
Allow user-defined notation that uses
lean.parserfor parsing its parameters and computes a pre-term in the tactic monad. The notation is activated by a singletkparser, which may optionally be preceded by aqexprparser for postfix/infix notations.Examples: the mandatory
unquote!macro, aformat!macro, and a non-creative infix notation example. More suggestions welcome.