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: Oct 13 2024 at 01:02 UTC