Zulip Chat Archive

Stream: mathlib4

Topic: Order.SupIndep mathlib4#1627


Ruben Van de Velde (Jan 17 2023 at 14:14):

I'm stuck on

def Independent {ι : Sort _} {α : Type _} [CompleteLattice α] (t : ι  α) : Prop :=
   i : ι, Disjoint (t i) ( (j) (_ : j  i), t j)

with error

elaboration function for 'Lean.Parser.Command.«termExpand_binders%(_=>_)_,_»' has not been implemented
  expand_binders% (f => supᵢ✝ f) (_ : j  i), t j

Any thoughts?

Patrick Massot (Jan 17 2023 at 14:17):

def Independent {ι : Sort _} {α : Type _} [CompleteLattice α] (t : ι  α) : Prop :=
   i : ι, Disjoint (t i) ( (j) (_H : j  i), t j)

will work, but maybe we now have a better solution (that was the state of the art solution one month ago).

Patrick Massot (Jan 17 2023 at 14:18):

At least this will get you unstuck.

Ruben Van de Velde (Jan 17 2023 at 14:19):

Huh, I thought I tried that. Thanks

Patrick Massot (Jan 17 2023 at 14:28):

Don't forget to let a porting note flagging this (unless @Mario Carneiro tells us there is a better solution now).

Mario Carneiro (Jan 17 2023 at 14:29):

oh, that's just a simple bug in the implementation, I hadn't heard about this before


Last updated: Dec 20 2023 at 11:08 UTC