Zulip Chat Archive

Stream: mathlib4

Topic: Missing lemmas

Jireh Loreaux (Jan 26 2023 at 17:19):

What should we do about missing lemmas? For example, there is no analogue of docs#subtype.ne_of_val_ne, at least not according to #align or my search of the docs. Should I just add it to Mathlib.Data.Subtype?

Mario Carneiro (Jan 26 2023 at 17:21):

that shouldn't happen if the previous file was ported

Mario Carneiro (Jan 26 2023 at 17:23):

sigh... it's another unported file from core

Mario Carneiro (Jan 26 2023 at 17:23):

init.data.subtype.basic should be ported to Mathlib.Init.Data.Subtype.Basic

Jireh Loreaux (Jan 26 2023 at 17:24):

okay, I can do that. Is oneshot the only way to get mathport to do it for me?

Mario Carneiro (Jan 26 2023 at 17:24):

no, the file is in lean3port

Jireh Loreaux (Jan 26 2023 at 17:40):

!4#1863

Arien Malec (Jan 26 2023 at 18:09):

Is there a comprehensive list of unported core files?

Jireh Loreaux (Jan 26 2023 at 18:51):

I guess you could just compare the filenames in the directories init and Mathlib.Init and normalize all filenames to be lowercase.

Last updated: Dec 20 2023 at 11:08 UTC