Stream: Coq users

Topic: `-<` notation in ITrees?

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}.

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

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.

Quinn (Jan 12 2022 at 18:00):

ok, thanks

Last updated: Oct 12 2024 at 12:01 UTC