Say I wanted my language to support various operator symbols, the semantics of which are defined by the user or by axioms.
I'm wondering whether Lean4 (or a typical well-known PA) just stores new kinds of operation expressions as strings, lists, expression trees or...? Could you link me to the specific part in the Lean4 code that defines these classes or structs?
I'm fairly certain that it doesn't implement a new class in its kernel for each operator, because it supports almost any Unicode string as an operator symbol (?)
So what data structure does lean use internally to represent the expressions that are the definition part of its lambda functions. I'm assuming it's based upon Lambda functions, because it's Type Theory-based, and usually or so I thought each of those systems appeals to these types expressions.
I am not sure whether I'll support every operator under the sun, but I at least want every operator appearing in Algebra by Serge Lang, for example. Well, they don't mention wreath product in that book, so in essence, your typical math book plus a few exotic operators. But it should be straight-forward to add in new operators, i.e. not a week-or-more of debugging to get them to work.
You can stop reading here, the below is just extra information
I'm not going to represent things as Unicode as Lean4 does, instead I'm going the LaTeX approach. Everything the user types in, there is a live preview that renders LaTeX / Markdown. If anyone is interested, the canonical example of such an editor (with no PA or any kind of math backend) is:
I did not come up with that on my own. It's an example provided by Qt, the markdown portion. I did add in support for KaTeX, but it was easy. If you'd like say to add in support for the Quiver editor on the JS side, you'd have to figure out how the QWebChannel communication code works.
I know a lot of math (check out my MSE profile). I have been coding for over 10 years. I know the essentials to get a DSL or programming language up and running, but have never actually finished & publically shared one. The D language has this nice parser generator called pegged, which allows you to specify PEG grammars. I am intermediate at it. It's a lot more user friendly to me than ANTLR or bison / lex. I by no means want to compete with Lean4 or anything. My goal is to do diagram chase-based proofs, but of course I need to support at least polynomials, and then a can of worms is opened into the world of PA's. I have coded many frontends for diagram editors, but always seem to get stuck on the logical backend or the PA-related system. A book recommendation would be nice. I think I want to stick with natural deduction and set theory axioms, and not delve into Type Theory quite yet. I would like the presentation of my system to be as close of a match to mathematics as-you-see-it in rigorous, formal-yet-human-readable textbooks.
So what I lack is "formalized logic theory" knowledge, Compiler Design, Type Theory knowledge. I figured I am good enough of a programmer to tackle what I need to, though, without taking graduate-level courses to understand some of this stuff. I figure, if I know math and I know how to program, then I should be able to come up with something. Just something that would be of value to mathematical users.