coq

Coq can't define an inductive proposition

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.

Solution

  • 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.