data.option.defs

Stream: mathlib4

[Scott Morrison]

@Jakob von Raumer, I noticed in the #port-status file you wrote that data.option.defs is blocked by init.data.option.instances. In some sense this isn't really blocked --- it just means someone needs to do that file first, so I'm not sure it makes sense to change the status away from No in this case.

In any case, I did that file as mathlib4#485, as an example that we can port stuff from Lean3 as well as mathlib3. There is a lean3port repository parallel to the mathlib3port repository, for exactly this purpose.

[Scott Morrison]

I just updated the #port-guide to mention this.

[Scott Morrison]

(Also, I think it was also you who marked category_theory.concrete_category.bundled as blocked by tactic.pi_instances. This is incorrect: you can easily remove that import from category_theory.concrete_category.bundled and everything works fine.)

[Scott Morrison]

(I made the trivial cleanup PR as #17093)

[Gabriel Ebner]

If you're looking at fies in core, you should look at the ported branch of lean3port: https://github.com/leanprover-community/lean3port/blob/ported/Leanbin/Init/Data/Option/Instances.lean

[Jakob von Raumer]

@Scott Morrison Thanks! I asked for something like lean3port yesterday but I think it got buried among other stuff