> > I'm not sure how to integrate that into a text editor like > interface, but it seems to be it'd be possible. > E.g., some sort of escape like a leading "!" that switches modes. >
Look how Jape did it: https://github.com/RBornat/jape/tree/master/dev/doc/manuals/roll_your_own Though, it might be overly complex. The UI in Jape is friendly but the language is not. I wouldn't try to write my own tactic in it. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/721c84e9-eee1-4297-b98c-2812d7578701%40googlegroups.com.
