• Robbert Krebbers's avatar
    Make the types of the finite map type classes more specific. · 20b4ae55
    Robbert Krebbers authored
    This makes type checking more directed, and somewhat more predictable.
    
    On the downside, it makes it impossible to declare the singleton on
    lists as an instance of SingletonM and the insert and alter operations
    on functions as instances of Alter and Insert. However, these were not
    used often anyway.
    20b4ae55
upred_big_op.v 16.6 KB