CoeDep instance for Fin n

Stream: new members

[Julia Scheaffer]

Is an instance like this a bad idea?

instance {n m : Nat} : CoeDep Nat n (Fin (n + Nat.succ m)) where
  coe := Fin.mk n (by omega)

I wanted it for some code I was writing and managed to generalize it in a way, but I think this might not be good for lean for some reason.

[Aaron Liu]

we got rid of the global Nat \to Fin coercion because it was messing with type inference

[Aaron Liu]

you could have something go Fin -> Nat -> Fin

[Julia Scheaffer]

Ah, i figured something like that might be the case

[Aaron Liu]

this seems like it's reintroducing the problem

[Julia Scheaffer]

lol yes probably

[Julia Scheaffer]

okay, i will just inline it. It's not like i'm using it that much yet, it just seemed like it would be possible

[Julia Scheaffer]

A CoeDep instance would stop it from chaining coercions together, right?

[Aaron Liu]

oh yeah

[Aaron Liu]

but you could have a coercion applied to a bound variable which is then instantiated with another coercion

[Julia Scheaffer]

This project is my first time using coercions, so I dont understand the system very well yet.