mcb icon indicating copy to clipboard operation
mcb copied to clipboard

Published 20 hours ago • verified publisher icon math-comp

Coercion nat_of_ord

Open gares opened this issue 3 years ago • 0 comments

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.

gares avatar May 18 '21 13:05 gares