Stream: math-comp users

Topic: Can I compute with nat_of_ord?


view this post on Zulip Shengyi Wang (May 08 2023 at 19:08):

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