Zulip Chat Archive

Stream: mathlib4

Topic: order.filter.germ


Yury G. Kudryashov (Jan 24 2023 at 04:47):

mathlib4#1799 is help-wanted, so I'm going to fix some compile errors.

Yury G. Kudryashov (Jan 24 2023 at 04:51):

What is the Lean 4 version of has_lift_t?

Arien Malec (Jan 24 2023 at 04:52):

MonadLiftT?

Yury G. Kudryashov (Jan 24 2023 at 04:53):

What "monad" means here?

Arien Malec (Jan 24 2023 at 04:56):

The types don't line up.... Grr.

Eric Wieser (Jan 24 2023 at 09:20):

docs4#MonadLiftT is presumably docs#has_monad_lift, not has_lift_t

Yury G. Kudryashov (Jan 24 2023 at 09:53):

It should be something like docs4#CoeTC but I'm not sure which one of these Coe* classes should I use.

Anne Baanen (Jan 24 2023 at 10:33):

Yury G. Kudryashov said:

What is the Lean 4 version of has_lift_t?`

I believe there is no direct equivalent of lift, where the coercion needs an explicit . I suppose we'll have to go for docs4#CoeTail since it's the best equivalent to the lean3 semantics, where the resulting type is fixed but the input type could be changed by further coercions. (I understand docs4#CoeTC is there for technical reasons, not meant for implementing further instances.)

Eric Wieser (Jan 24 2023 at 11:07):

My guess would be that there is no such thing as lift for the same reason that there is no such thing as coe

Eric Wieser (Jan 24 2023 at 11:08):

I think you're expected to write a function with a name for lift_ts

Eric Wieser (Jan 24 2023 at 11:08):

Oh nevermind, lift_t still has a place because it's transitive

Eric Wieser (Jan 24 2023 at 11:08):

Maybe we should just forward-port lift_t?


Last updated: Dec 20 2023 at 11:08 UTC