Zulip Chat Archive

Stream: mathlib4

Topic: mathlib4#793

Scott Morrison (Nov 30 2022 at 02:38):

@Yaël Dillies, I just saw that you are working on porting Order.Heyting.Basic, sorry. I've basically done it at mathlib4#793.

Scott Morrison (Nov 30 2022 at 02:39):

From the PR description, the remaining items are:

  • Wait for nightly-2022-11-30 to arrive, which will solve most of the errors.
  • Either port pi_instance, or do without.
  • Either port refine_struct, or do without.

Yaël Dillies (Nov 30 2022 at 02:40):

Whoops. I guess we got lucky that supervision work meant I couldn't start it today as I thought I would.

Last updated: Dec 20 2023 at 11:08 UTC