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