coqdependent-typetheorem-proving

Is there any difference between "parameters" and "indices" in Coq theorems?

I am perfectly familiar with the deal of distinguishing parameters from indices while declaring inductive types. What I am unsure about is whether there is any difference between putting things before vs after colon when declaring theorems. Specifically

Lemma par (n : nat) : n < 1 -> n = 0.

Lemma ind : forall (n : nat), n < 1 -> n = 0.

One difference I found is that when proving par, everything on the right of the colon is initially in the context, while in ind I have to intro it. Do you know any other differences between these two? Can you make an example where it matters more than just a bunch of intro/revert?

One of my concerns is that automation might prefer one over another, eg autorewrite or auto, though I couldn't find an example where that would make a difference.

Solution

  • See the documentation:

    The form Definition ident binders : type := term is equivalent to Definition ident : forall binders, type := fun binders => term.