I want to use the `ordinal`

type in my project since I can define finite functions with this type. However, I also want to compute with it. I know it is not hard to prove `nat_of_ord (inord n) = n`

. For example:

```
Goal nat_of_ord (inord 2 : 'I_5) = 2%nat.
Proof. by rewrite inordK. Qed.
```

But when I try `Eval compute in nat_of_ord (inord 2 : 'I_5).`

, I did not get 2 as I expected. Is there any way to evaluate it to get 2? Thanks.

Last updated: Jul 25 2024 at 15:02 UTC