Commit 2022-12-07 03:37 d95a1654

View on Github →

feat: port Control.Traversable.Basic (#788) thing copied from mathlib3port: 1fc36cc9c8264e6e81253f88be7fb2cb6c92d76a

Depends on: #803 (for list.traverse)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Control/Traversable/Basic.lean

added theorem ApplicativeTransformation.app_eq_coe

added theorem ApplicativeTransformation.coe_inj

added theorem ApplicativeTransformation.coe_mk

added def ApplicativeTransformation.comp

added theorem ApplicativeTransformation.comp_apply

added theorem ApplicativeTransformation.comp_assoc

added theorem ApplicativeTransformation.comp_id

added theorem ApplicativeTransformation.ext

added theorem ApplicativeTransformation.ext_iff

added def ApplicativeTransformation.idTransformation

added theorem ApplicativeTransformation.id_comp

added theorem ApplicativeTransformation.preserves_map'

added theorem ApplicativeTransformation.preserves_map

added theorem ApplicativeTransformation.preserves_pure

added theorem ApplicativeTransformation.preserves_seq

added structure ApplicativeTransformation

added def sequence