xixejas (Oct 01 2022 at 16:22): 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?
Paolo Giarrusso (Oct 01 2022 at 16:59):it should be possible... %coq_nat suggests you might be mixing stdlib functions with ssreflect functions?
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)
Paolo Giarrusso said:
it should be possible...
%coq_natsuggests 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
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
Kenji Maillard (Oct 01 2022 at 18:44):reflect goes both ways
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.
Notification Bot (Oct 01 2022 at 20:09):xixejas has marked this topic as resolved.
Last updated: Dec 05 2023 at 11:01 UTC