Unfolding instance notation

Stream: Is there code for X?

[Thomas Vigouroux]

Hey there, I have implemented Bot T for some T but at some point in the proof I'd like to replace \bot (the notation) with it's actual definition (in the instance), how'd I do that ?

[Kevin Buzzard]

If you implemented it (ie made a definition) then your next job is to write the API for that definition, so you could make a lemma saying (\bot : T) = <its definition>, prove it with rfl, and now you can rewrite with that lemma to do what you want to do.

[Thomas Vigouroux]

Oh okay, I have to do that manually then, thanks !

[Kevin Buzzard]

Alternatively you could just use a tactic like change to make the change, but in general it's best to make the API I guess, because it leads to cleaner code.

[Thomas Vigouroux]

Yeah, implementing the API seems to be the best here, is greatly helps

[Thomas Vigouroux]

Now that's weird though, related to this problem, I get that bot \in A is different than T.bot \in A, which seems to be the case ?

[Kevin Buzzard]

#mwe ?

[Thomas Vigouroux]

Nvm, it was just me being dumb!