Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-12-17 10:50 53b08c1c

View on Github →

fix(*): untangle dependency hierarchy

Estimated changes

Modified algebra/group.lean

Modified category/traversable/basic.lean

Modified category/traversable/instances.lean

Deleted core/data/list.lean

deleted def list.partition_map

Deleted core/default.lean

Modified data/equiv/basic.lean

Modified data/list/basic.lean

deleted inductive list.forall₂

Modified data/list/defs.lean

added inductive list.forall₂

added def list.partition_map

Modified data/nat/basic.lean

Renamed data/option.lean to data/option/basic.lean

deleted def option.filter

deleted def option.guard

deleted def option.iget

deleted theorem option.iget_some

deleted theorem option.is_none_iff_eq_none

deleted def option.lift_or_get

deleted theorem option.mem_def

deleted theorem option.mem_to_list

deleted inductive option.rel

deleted theorem option.some_inj

deleted def option.to_list

Created data/option/defs.lean

added def option.filter

added def option.guard

added def option.iget

added theorem option.iget_some

added theorem option.is_none_iff_eq_none

added def option.lift_or_get

added theorem option.mem_def

added theorem option.mem_to_list

added inductive option.rel

added theorem option.some_inj

added def option.to_list

Modified data/pfun.lean

Modified data/prod.lean

modified theorem prod.ext

Modified logic/embedding.lean

Modified logic/function.lean

Modified meta/rb_map.lean

Modified order/bounded_lattice.lean

Modified tactic/auto_cases.lean

Modified tactic/chain.lean

Modified tactic/ext.lean

Modified tactic/interactive.lean

Modified tactic/pi_instances.lean

Created tactic/simpa.lean

Modified tactic/squeeze.lean