Stream: math-comp users

Topic: measure ssrnat


view this post on Zulip xixejas (Oct 01 2022 at 16:22):

I'm trying to do a Function ... {measure ...} with ssrnat, but when I open the Proof section I get a %coq_nat and I can't do anything with it. Is it possible to define functions like this with ssrnat?

view this post on Zulip Paolo Giarrusso (Oct 01 2022 at 16:59):

it should be possible... %coq_nat suggests you might be mixing stdlib functions with ssreflect functions?

view this post on Zulip Ana de Almeida Borges (Oct 01 2022 at 17:49):

I would also like to know the answer to your question, but in the meantime, you can translate between coq_nat and nat. Just Search for both. For example:

Search (_ < _)%coq_nat (_ < _).

gives us

ltP: forall {m n : nat}, reflect (m < n)%coq_nat (m < n)

view this post on Zulip xixejas (Oct 01 2022 at 18:39):

Paolo Giarrusso said:

it should be possible... %coq_nat suggests you might be mixing stdlib functions with ssreflect functions?

That was also my reaction, but I've Checked virtually everything and nothing else shows the %coq_nat

view this post on Zulip xixejas (Oct 01 2022 at 18:42):

Ana de Almeida Borges said:

ltP: forall {m n : nat}, reflect (m < n)%coq_nat (m < n)

Unfortunately that goes in the option direction of what I need

view this post on Zulip Kenji Maillard (Oct 01 2022 at 18:44):

reflect goes both ways

view this post on Zulip xixejas (Oct 01 2022 at 18:46):

This is magic. I'm sure I tried it 5 times and it only worked after your message.


Last updated: Jan 29 2023 at 18:03 UTC