zmod

Stream: general

[petercommand]

https://github.com/leanprover/mathlib/blob/master/data/zmod/basic.lean#L302
Why is there an explicit argument (underscore) to eq_iff_modeq_int here?
When I move cursor onto eq_iff_modeq_int at line 302, the type of eq_iff_modeq_int is inferred with an extra (hp : prime p), but that argument isn't there when I jump to the def of eq_iff_modeq_int

[Moses Schönfinkel]

Because line 224 declares a variable (hpp : prime p).

[petercommand]

but eq_iff_modeq_int is defined outside of this file

[petercommand]

oh sorry, it's defined in the same file

[petercommand]

thanks!

[petercommand]

:D