Zulip Chat Archive

Stream: mathlib4

Topic: data.fin.vec_notation mathlib4#1741


Johan Commelin (Jan 21 2023 at 05:21):

I started this PR, but I need help with the notation.

Johan Commelin (Jan 21 2023 at 08:26):

There's some stuff left about:

  • a Repr instance
  • unsafe defs
  • bit0/bit1 stuff

Johan Commelin (Jan 21 2023 at 08:26):

Help appreciated!

Eric Wieser (Jan 21 2023 at 08:59):

I can maybe take a look at the repr instance

Eric Wieser (Jan 21 2023 at 09:31):

Done

Eric Wieser (Jan 21 2023 at 09:32):

I think it's probably reasonable to comment out the two unsafe instances for now; I think has_reflect (now docs4#Lean.ToExpr) has been made redundant somehow by Qq, although I don't really understand why

Johan Commelin (Jan 21 2023 at 09:38):

What about the to_pexpr stuff?

Eric Wieser (Jan 21 2023 at 10:03):

This was all prework for my mathlib3 meta matrix PR

Eric Wieser (Jan 21 2023 at 10:04):

So I think commenting it out with a porting note and maybe a TODO(eric-wieser) is fine

Eric Wieser (Jan 21 2023 at 10:08):

I suspect the replacement is a function from fin n → Q(α) to Q(fin n → α); maybe @Gabriel Ebner can comment on what that would look like.

Eric Wieser (Jan 21 2023 at 10:10):

(but no need to hold up the PR for that)

Johan Commelin (Jan 21 2023 at 10:21):

done

Johan Commelin (Jan 21 2023 at 10:22):

The only stuff remaining is the bit0/bit1 warnings

Johan Commelin (Jan 23 2023 at 14:27):

Who's gonna merge this?

Eric Wieser (Jan 23 2023 at 14:28):

Should we do the backport first?

Eric Wieser (Jan 23 2023 at 14:28):

Otherwise we'll have porting notes that refer to something that doesn't exist any more, which is a bit confusing

Johan Commelin (Jan 23 2023 at 14:29):

I think the API change isn't big enough to require a backport

Johan Commelin (Jan 23 2023 at 14:29):

Or at least, it doesn't need to hold up the port

Ruben Van de Velde (Jan 23 2023 at 16:40):

@Johan Commelin I reverted the change, but now I'm not sure if I should merge it myself :)

Yury G. Kudryashov (Jan 23 2023 at 16:44):

I think, it's OK for you to merge it.

Ruben Van de Velde (Jan 23 2023 at 16:45):

Oh, bors doesn't think I can anyway


Last updated: Dec 20 2023 at 11:08 UTC