Zulip Chat Archive

Stream: mathlib4

Topic: data.option.defs


Scott Morrison (Oct 21 2022 at 01:29):

@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 (Oct 21 2022 at 01:32):

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

Scott Morrison (Oct 21 2022 at 01:37):

(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 (Oct 21 2022 at 01:40):

(I made the trivial cleanup PR as #17093)

Gabriel Ebner (Oct 21 2022 at 02:02):

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 (Oct 21 2022 at 07:35):

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


Last updated: Dec 20 2023 at 11:08 UTC