search

math-comp / mcb

Mathematical Components (the Book)
Other
139 stars 25 forks source link

Coercion nat_of_ord #116

Open gares opened 3 years ago

gares commented 3 years ago

https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/reading.20mathcomp.20book

It should be

Coercion nat_of_ord n (i : 'I_n) := let: @Ordinal _ m _ := i in m.