This is just a mundane syntax question. Is there something similar to
Example x : foo., except it doesn’t require me to give a name to the example? I’d like to have a number of trivial examples/tests, and find it annoying to write
Example ex2, etc.
I am aware of
Goal foo, but I was hoping to keep “example” or a similar keyword, just to clarify that the goal is illustrative.