search

verified-network-toolchain / petr4

Petr4: Formal Semantics for P4
Apache License 2.0
73 stars 20 forks source link

Functor Notations #421

Closed zachary-kent closed 1 year ago

zachary-kent commented 1 year ago

Adds an infix operators for (applicative) functors

hackedy commented 1 year ago

Do you want to add an applicative typeclass, or is it just for monad operations?

zachary-kent commented 1 year ago

Do you want to add an applicative typeclass, or is it just for monad operations?

Do you think it would be worth adding an applicative typeclass? Also, do you know if there's a reason we rolled our monads instead of using the definitions in say coq-ext-lib?

hackedy commented 1 year ago

I think a standalone Applicative typeclass is probably not worth it.

My impression was that ext-lib doesn't provide that much beyond what we have. I'd be interested in using stdpp or something like that though.

zachary-kent commented 1 year ago

I think a standalone Applicative typeclass is probably not worth it.

My impression was that ext-lib doesn't provide that much beyond what we have. I'd be interested in using stdpp or something like that though.

Makes sense. Do you think this is good to merge then?