Commit 2024-04-05 20:49 9821d04c

View on Github →

chore(Data/List/Func): Delete (#11847) This file was used in the Lean 3 implementation of omega and nowhere else. It's mathematically redundant with Data.List.ToFinsupp.

Estimated changes

deleted def List.Func.Equiv
deleted def List.Func.add
deleted theorem List.Func.add_nil
deleted theorem List.Func.eq_get_of_mem
deleted theorem List.Func.eq_of_equiv
deleted theorem List.Func.equiv_of_eq
deleted theorem List.Func.equiv_refl
deleted theorem List.Func.equiv_symm
deleted theorem List.Func.equiv_trans
deleted def List.Func.get
deleted theorem List.Func.get_add
deleted theorem List.Func.get_map'
deleted theorem List.Func.get_map
deleted theorem List.Func.get_neg
deleted theorem List.Func.get_nil
deleted theorem List.Func.get_pointwise
deleted theorem List.Func.get_set
deleted theorem List.Func.get_sub
deleted theorem List.Func.length_add
deleted theorem List.Func.length_neg
deleted theorem List.Func.length_set
deleted theorem List.Func.length_sub
deleted theorem List.Func.map_add_map
deleted theorem List.Func.mem_get_of_le
deleted def List.Func.neg
deleted theorem List.Func.nil_add
deleted theorem List.Func.nil_pointwise
deleted theorem List.Func.nil_sub
deleted def List.Func.pointwise
deleted theorem List.Func.pointwise_nil
deleted def List.Func.set
deleted def List.Func.sub
deleted theorem List.Func.sub_nil