Commit 2023-01-19 05:02 def691e8

View on Github →

feat: port Control.Traversable.Instances (#1393)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Control/Traversable/Instances.lean

added theorem List.mem_traverse

added theorem List.traverse_append

added theorem List.traverse_cons

added theorem List.traverse_nil

added theorem Option.comp_traverse

added theorem Option.id_traverse

added theorem Option.naturality

added theorem Option.traverse_eq_map_id