fsdoc: no-summary-found
fsdoc: no-comment-found
* FStar.IFC provides a simple, generic abstraction * for monadic information-flow control * based on a user-defined (semi-)lattice of information flow labels *