differentiate unlocked theorems from axioms in theorem list

[mcol]

For example, pow_zero shows this text: "pow_zero a : a ^ 0 = 1 is one of the two axioms defining exponentiation in this game." If pow_zero is indeed an axiom, perhaps it should have a different colour or icon, to differentiate it from the unlocked theorems.

[joneugster]

This is an interesting point. I guess for game play it doesn't really matter what are axioms and what are theorems.

Making them colourful might draw too much attention on them when the attention should rather go to the newly introduced theorems (which are colourful in the next update)

[mcol]

I agree, colour would not work well. Perhaps as a tooltip? But feel free to close if this suggestion goes beyond or against the objectives of the game.

[joneugster]

That's a good idea. At the place in lean4game where the signature is autogenerated, one could also check whether the statement is an axiom.