Open semorrison opened 5 years ago
I like the idea of giving a different name to proofs. Would you call both 0-cells made with the plus button and cells made with source
/target
generators? I am not sure this gains much over calling them cells. For theorems I would suggest that the theorem statement be called theorem n
and it's proof be called proof n
Currently new cells receive default names
Cell n
. This could be changed to produceGenerator n
(if created usingtarget
), orDefinition n
/Proof n
(if created usingtheorem
).This would indicate to the user the "natural interpretation" of the cells when the system is thought of as an interactive theorem prover. The fact that these interpretations were only shown in the "meaningless" user-facing name might ensure the user doesn't mistakenly come to believe that the different types of cells actually behave any differently during the rest of the interaction.