- we need a special name-space for builtin thingies. E.g. when we print a "Sort (...)" usually it can be printed as "Type" or "Type1" but these vars may be hidden. We currently print them as "<Type>" or some such, but it's not an "official" syntax. I think we need an official syntax (one that works when reading a program) that stands for "builtin". It could be "##..." or "<...>" (i.e. a special naming convention) or "(## ...)" or the "(built-in ...)" we currently use. The important thing is that it should also be usable to represent the Sort(...) and SortLevel(...) lexps. And it should be sufficiently concise to be tolerable in printed output. I'm leaning towards "##" so we'd write "##Type ##0", "##Type (##S ##0)", "##+", "##TypeLevel", ... OTOH, since I plan on using "." for module-field names, we could use a ".." prefix and write things like "..Type ..0".
Plus j'y pense plus ça me plait: "inductive-cons" devient "##cons", "inductive_" devient "##inductive" ou "##datatype". Et ce ne sont pas des variables, donc ça ne peut pas être redéfini.
Stefan