Zulip Chat Archive

Stream: PR reviews

Topic: !4#4723 FieldTheory.Adjoin

Riccardo Brasca (Jun 06 2023 at 15:42):

I am done for today with !4#4723. If someone wants to continue please go ahead. This file is needed for a lot of Galois theory/ algebraic number theory.

It's not very difficult, but quite annoying, essentially every declaration needs to be fixed. Note that mathport translated K⟮x⟯ with K⟮⟯, adding the line

/- ./././Mathport/Syntax/Translate/Expr.lean:192:11: unsupported (impossible) -/

Ruben Van de Velde (Jun 06 2023 at 15:54):

I've got about five minutes

Ruben Van de Velde (Jun 06 2023 at 16:01):

Free again

Riccardo Brasca (Jun 06 2023 at 16:03):

I don't know if we want to fix the mathport problem, it's maybe easier to fix all the K⟮⟯ by hand.

Damiano Testa (Jun 06 2023 at 16:20):

I'll take a look at this for a little bit.

Damiano Testa (Jun 06 2023 at 17:29):

I am going to stop: this has been a very unsatisfying and failed attempt!

Riccardo Brasca (Jun 06 2023 at 19:06):

Thanks!

Riccardo Brasca (Jun 07 2023 at 09:00):

I've made some progress, but I have to stop again.

Riccardo Brasca (Jun 08 2023 at 08:04):

@Chris Hughes I see you are working on this now. If you have other things to do I can finish it (hopefully)

Riccardo Brasca (Jun 08 2023 at 08:04):

But thanks!

Riccardo Brasca (Jun 08 2023 at 08:05):

Oh, it already compiles, great!!

Chris Hughes (Jun 08 2023 at 08:06):

There's some simpNFs left

Chris Hughes (Jun 08 2023 at 08:08):

It's not that obvious to me how to fix them because I'm not familiar with the notation here.

Riccardo Brasca (Jun 08 2023 at 08:11):

Having a look

Riccardo Brasca (Jun 08 2023 at 09:39):

It should be ready for review.

Last updated: Dec 20 2023 at 11:08 UTC