• Robbert Krebbers's avatar
    More stuff for indexed products. · 1cfbdb17
    Robbert Krebbers authored
    * Insert and singleton operation.
    * Identity element.
    * Non-expansiveness and properness of insert and singleton.
    * Frame preserving updates.
    * Functoriality.
    1cfbdb17
fin_maps.v 10.6 KB