Stream: math-comp users

Topic: Windows mathcomp version


view this post on Zulip Raul (Mar 29 2023 at 16:35):

I repeat here my question, so that anyone can see it:

Raul said:

Hello!!
I'm using the version from the school in my Windows system and the last version from Coq in the WSL.
For reasons I don't understand, the [ 'subType' 'for' _ ] Notation doesn't exist in my Windows's Coq, but my mathcomp's tutorial pdf is from 2021 and already has it.

What do I do?
I would love being able to continue working on it on Windows.

view this post on Zulip Laurent Théry (Mar 30 2023 at 12:21):

Which tutorial you are talking about. I am trying to maintain upto date version of tutorials here. It works with coq 8.16 and mathcomp 1.16.

view this post on Zulip Laurent Théry (Mar 30 2023 at 12:51):

Look like in your HB version it has been renamed [ 'isSub' 'for' v ]


Last updated: Jul 25 2024 at 15:02 UTC