For grasshopper etc. it would be useful for symbols to be more than just strings with attached variables, but instead allow for proper interpolation of those variables into the symbol to 'unfold' it into part of the output proof. This would require creating a mini-language of escape sequences in the symbol that cause it to substitute variables, and making the parser aware of this.
For grasshopper etc. it would be useful for symbols to be more than just strings with attached variables, but instead allow for proper interpolation of those variables into the symbol to 'unfold' it into part of the output proof. This would require creating a mini-language of escape sequences in the symbol that cause it to substitute variables, and making the parser aware of this.