Stream: Coq users

Topic: `-<` notation in ITrees?


view this post on Zulip Quinn (Jan 12 2022 at 02:43):

I'm reading ITrees. What does -< mean?

    Context {E : Type -> Type}.
    Context {HasReg : Reg -< E}.
    Context {HasMemory : Memory -< E}.
    Context {HasExit : Exit -< E}.

view this post on Zulip Li-yao (Jan 12 2022 at 03:05):

It's a type class Reg -< E that unfolds to a function forall T, Reg T -> E T

view this post on Zulip Li-yao (Jan 12 2022 at 03:06):

You can think of E as a "set of effects" and those instances mean that it contains Reg, Memory and Exit effects.

view this post on Zulip Quinn (Jan 12 2022 at 18:00):

ok, thanks


Last updated: Jan 28 2023 at 06:30 UTC