Documentation

FormaleSystemeInLean.List

This file contains auxiliary results about lists that do not have anything to do with Formale Systeme.

source
theorem List.removeAll_nil_flatten {α : Type u_1} [BEq α] (l : List (List α)) :
(l.removeAll [[]]).flatten = l.flatten

Removing all occurrences of [[]] from a list before applying flatten does not change the result of flatten.

source
def List.removeDups {α : Type u_1} [DecidableEq α] :
List α → List α

Eliminates duplicates from a list, keeping the rightmost occurrence. (Implementation copied from https://github.com/monsterkrampe/Basic-Lean-Datastructures/blob/main/BasicLeanDatastructures/List/EraseDupsKeepRight.lean)

Equations
Instances For
    source
    theorem List.mem_removeDups {α : Type u_1} [DecidableEq α] (l : List α) (a : α) :
    a ∈ l ↔ a ∈ l.removeDups

    Removing duplicates from a list does not change the elements contained in it.

    source
    theorem List.removeDups_count {α : Type u_1} [DecidableEq α] (l : List α) (a : α) :
    a ∈ l → count a l.removeDups = 1

    In a list with removed duplicates, each element has count 1.

    source
    theorem List.removeDups_nodup {α : Type u_1} [DecidableEq α] (l : List α) :
    l.removeDups.Nodup
    source
    @[implicit_reducible]
    instance List.decidableInfix {α : Type u_1} [DecidableEq α] (k l : List α) :
    Decidable (k <:+: l)

    Infix is decidable for Lists whose elements have decidable equality. (The proof is essentially the expanded version of the one from mathlib)

    Equations