blob: 9bee5bd5bb31df688f32f5f0ec943c2ee979f3b3 [file] [edit]
modBug.lean:1:48-1:64: error: application type mismatch
Nat.zero_ne_one (Nat.mod_zero 1)
argument
Nat.mod_zero 1
has type
1 % 0 = 1 : Prop
but is expected to have type
0 = 1 : Prop