Commit 2023-01-27 14:47 50036b41

View on Github →

chore: Rename Type* to Type _ (#1866) A bunch of docstrings were still mentioning Type*. This changes them to Type _.

Estimated changes

modified structure CoolerHom
modified theorem do_something
modified theorem map_cool
modified theorem map_op
modified structure CoolerEmbedding
modified theorem do_something
modified theorem map_cool
modified theorem map_op
modified structure CoolerIso
modified theorem do_something
modified theorem map_cool
modified theorem List.not_mem_keys_kerase