Documentation

VCVio.OracleComp.SimSemantics.WriterT

Simulation using WriterT Monad Transformers #

Lemmas about simulateQ with output monad WriterT ω (OracleComp spec) for some ω

Note we only handle monoid version of WriterT, append should be added eventually.