Commit 2022-11-30 16:55 c8e9a357

View on Github →

feat: port Control.Applicative (#798) mathlib3 SHA: 4e42a9d0a79d151ee359c270e498b1a00cc6fa4e A couple of changes needed to be made because Seq.seq now has a Unit argument. There remain some sorries that were previously solved by control_laws_tac.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Control/Applicative.lean

added theorem Applicative.ext

added theorem Applicative.map_seq_map

added theorem Applicative.pure_seq_eq_map'

added theorem Comp.seq_mk

added theorem Functor.Comp.applicative_comp_id

added theorem Functor.Comp.applicative_id_comp

added theorem Functor.Comp.map_pure

added theorem Functor.Comp.pure_seq_eq_map

added theorem Functor.Comp.seq_assoc

added theorem Functor.Comp.seq_pure