My Coq compiler is not allowing for inductive propositions as:
Inductive relation : nat -> nat -> Prop :=
| A : relation 1 2
| B : relation 2 3.
Throws: Error: The reference B was not found in the current environment.
Inductive le : nat -> nat -> Prop :=
| le_n (n : nat) : le n n
| le_S (n m : nat) : le n m -> le n (S m).
Throws: Error: The reference m was not found in the current environment.
My previously running code is not breaking in all the ind. propositions. I don't know if something changed, I'm running these versions:
The Coq Proof Assistant, version 8.18.0
compiled with OCaml 5.1.0
Any ideas?
If I use only one rule as:
Inductive relation : nat -> nat -> Prop :=
| A : relation 1 2.
Works. So I tried changing from tabs to spaces. I didn't change the Coq version because this is the version that was actually compiling some days ago.
I suspect you have defined a funky notation involving the symbol "|", which confuses Coq as to how it should parse your declaration, and lead it to try to see the name of the constructor as a term.
For instance, the following triggers the error you mention:
Notation "a | c" := (a + c) (at level 0).
Inductive relation : nat -> nat -> Prop := | A : relation 1 2 | B : relation 2 3.