order.filter.germ

Stream: mathlib4

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

What is the Lean 4 version of has_lift_t?

[Arien Malec]

MonadLiftT?

[Yury G. Kudryashov]

What "monad" means here?

[Arien Malec]

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

[Eric Wieser]

docs4#MonadLiftT is presumably docs#has_monad_lift, not has_lift_t

[Yury G. Kudryashov]

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

[Anne Baanen]

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]

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]

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

[Eric Wieser]

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

[Eric Wieser]

Maybe we should just forward-port lift_t?