Anonymous example

Using Coq
1

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 ex1, 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.

2

Maybe Check is what you are looking for?

Here is a quick example with propositions:

Parameter A B : Prop.

Axiom axiom : A -> B.

(* proving A->B *)
Example ex : A -> B.
Proof. apply axiom. Qed.

(* "checking" A->B *)
Check axiom : A -> B.
Fail Check axiom : B -> A.