Finite types

Stream: Is there code for X?

[Ben]

How do finite types work in lean 3? #check (100: fin 8) is being passed as valid which is unexpected?

[Mario Carneiro]

fin 8 is the set of natural numbers less than 8, but 100 doesn't mean what you think there

[Mario Carneiro]

it actually means 100 % 8 = 4

[Mario Carneiro]

this is because numeral desugaring is defined generically for anything with a 0,1,+, and fin n (for n>0) has these operations defined via modulo arithmetic

[Mario Carneiro]

If you want the natural number 100, you should write #check (⟨100, _⟩ : fin 8) where the _ is a proof obligation of 100 < 8 that of course you can't fill

[Ben]

Interesting, I did not know it did that to the number in that way. That makes sense now :thumbs_up: