Hello everyone,

I am new to coq and I am following MIT 6.826

coq doesn't like this line:

```
Require Import Omega.
```

It says *Cannot find a physical path bound to logical path Omega*.

Is Omega depreciated or something ? my current coqc is 8.15.0

It has been replaced by Lia (and the `omega`

tactic by `lia`

).

well I replaced the require statement but there is some other problems that I don't fully understand:

```
Class EqualDec A :=
equal_dec : forall x y : A, { x = y } + { x <> y }.
(**
We define the notation [x == y] to mean our decidable equality
between [x] and [y].
*)
Notation " x == y " := (equal_dec (x :>) (y :>)) (no associativity, at level 70).
```

coq doesn't like the `:>`

part on the last line I would imagine that this is part of the removed syntax in `Omega`

?

I am not even sure what to google because `:>`

doesn't give much clues

`:>`

is a very obscure feature of Coq which no one really understood what it was doing, so it got removed. It is unrelated to Omega.

Alright thanks, I will take this as a sign that perhaps I should install the exact coq version they used, It would be hard to learn and troubleshoot at the same time.

Yep, that's the correct conclusion

@walker : if you tell me what Coq version it was, I can add it to the current Coq Platform (there was some discussion on how far back we should go).

8.12.0

OK, that is already included (that is you can install this version of Coq from sources with the latest Coq Platform scripts - or you can use the published Coq Platform installers for 8.12).

Alright thanks, I will get it from there!

walker has marked this topic as resolved.

walker has marked this topic as unresolved.

walker has marked this topic as resolved.

Last updated: Jun 15 2024 at 08:01 UTC