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?
it should be possible... %coq_nat
suggests you might be mixing stdlib functions with ssreflect functions?
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_nat
suggests you might be mixing stdlib functions with ssreflect functions?
That was also my reaction, but I've Check
ed virtually everything and nothing else shows the %coq_nat
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
reflect goes both ways
This is magic. I'm sure I tried it 5 times and it only worked after your message.
xixejas has marked this topic as resolved.
Last updated: Dec 05 2023 at 11:01 UTC