porting has_reflected and friends

Stream: mathlib4

[Adam Topaz]

I'm trying to get started porting, and one of the next files on the list is order.with_bot, which has the following instance fairly high up in the file:

meta instance {α : Type} [reflected _ α] [has_reflect α] : has_reflect (with_bot α)
| ⊥ := `(⊥)
| (a : α) := `(coe : α → with_bot α).subst `(a)

How should one go about porting this? Mathport produced the following output:

unsafe instance {α : Type} [reflected _ α] [has_reflect α] : has_reflect (WithBot α)
  | ⊥ => q(⊥)
  | (a : α) => q((coe : α → WithBot α)).subst q(a)

[Scott Morrison]

Just delete.

[Scott Morrison]

It's meta code, so to whatever extent it is needed it will be ported outside of the main theory porting effort.

[Adam Topaz]

Great!

[Adam Topaz]

I've ported the ToFormat instance as follows:

unsafe instance [Std.ToFormat α] :
    Std.ToFormat (WithBot α) where format x :=
    match x with
    | none => "⊥"
    | some x => Std.format x

Should I delete that as well?

[Patrick Massot]

Is it really "just delete" or "comment out and leave a porting note"?

[Scott Morrison]

I think the main value of leaving a porting note would just be that no one looking at the file later wonders if they were meant to leaving a porting note. :-) I'm not too concerned about stray meta code not being reflected in ported theory files. But if anyone has concerns about this we can easily declare that porting notes should be left, too.

[Kevin Buzzard]

my instinct at this point is to leave a porting note when anything diverges from the mathlib3port in pretty much any way other than issues involving the naming convention...

[Yaël Dillies]

Yeah, this instance was introduced by a PR of mine specifically dedicated to adding those meta instances. So it would be a shame to silently drop it.

[Adam Topaz]

(As it turns out, this file depends on tactic.lift, so I'm going to give up on porting it for now)

[Adam Topaz]

I don't know much about reflected and has_reflect from mathlib3, but is the intention that Qq will replace all of this stuff in Mathlib4?

[Scott Morrison]

Yes, as far as I understand there is no direct conversion of reflected and has_reflect, and so dropping them is the right thing to do.

[Eric Wieser]

I think docs4#Lean.ToExpr a pretty literal translation of the two of those classes together

[Eric Wieser]

If you did want to port it, it would look very similar to the code for the ToExpr instance for option

[Eric Wieser]

Isn't this what #noalign is for; to indicate that we deliberately didn't port it? Or do we already not both to align instances?