fin_arrow vs fin_pi

Stream: general

[Yaël Dillies]

Aren't docs#encodable.fin_arrow and docs#encodable.fin_pi creating a (not even propeq) diamond?

[Yaël Dillies]

Also, can't both be generalized by

instance pi.encodable (ι : Type*) (π : ι → Type*) [decidable_eq ι] [fintype ι] [encodable ι]
  [Π i, encodable (π i)] : encodable (Π i, π i) := sorry

[Alex J. Best]

Thats docs#fintype_pi . You need to pick some order on iota right? So if you want a computable instance you have to stick to fin, unless there is some succ_order generalization?

[Yaël Dillies]

Read carefully. I added [encodable ι].

[Reid Barton]

A finite encodable type has an ordering that can be used for this purpose

[Yaël Dillies]

and you get the current instances out of mine using docs#encodable.trunc_encodable_of_fintype

[Eric Wieser]

Having just read your PR that adds docstrings and renames, your generalization looks like a good one to me

[Yaël Dillies]

Okay I will try it then :smiling_face: