Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-06-11 14:05 9546e625

View on Github →

feat(data/list): add parametricity rules for list operations

Estimated changes

Modified data/list/basic.lean

added theorem list.bi_unique_forall₂

added theorem list.filter_map_cons

added theorem list.forall₂_cons_left_iff

added theorem list.forall₂_cons_right_iff

added theorem list.forall₂_eq_eq_eq

added theorem list.forall₂_flip

added theorem list.forall₂_map_left_iff

added theorem list.forall₂_map_right_iff

deleted theorem list.forall₂_nil_left

added theorem list.forall₂_nil_left_iff

deleted theorem list.forall₂_nil_right

added theorem list.forall₂_nil_right_iff

added theorem list.forall₂_refl

added theorem list.forall₂_same

added theorem list.left_unique_forall₂

added theorem list.rel_append

added theorem list.rel_bind

added theorem list.rel_filter

added theorem list.rel_filter_map

added theorem list.rel_foldl

added theorem list.rel_foldr

added theorem list.rel_join

added theorem list.rel_map

added theorem list.rel_mem

added theorem list.rel_nodup

added theorem list.rel_prod

added theorem list.rel_sections

added theorem list.right_unique_forall₂