Search code examples
coq

Coq: Cannot infer an internal placeholder of type "nat" in environment: ev : nat -> Prop

I am trying to execute IndProp.v of Software Foundation classes, but I am immediately greeted with error

Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
From LF Require Export Logic.
From Coq Require Import Lia.

...

Inductive ev : nat -> Prop :=s
  | ev_0 : ev 0
  | ev_SS (n : nat) (H : ev n) : ev (S (S n)).
===============================================

Cannot infer an internal placeholder of type "nat" in environment:
ev : nat -> Prop

I ve had some errors with core types being shadowed by those defined in the book before, but haven't seen this error before?

Previous chapters compile correctly.

denis@dgecko:~/books/Volume1_LogicalFoundations> coqc --version
The Coq Proof Assistant, version 8.14.0
compiled with OCaml 4.13.1
Solution

  • There is a spurious "s" after the := sign.