definition of a strict subset of a list

Stream: Is there code for X?

[Paige Thomas]

I was just wondering why there doesn't seem to be a definition for a list being a strict subset of another list?

[Paige Thomas]

That is, is it for math reasons?

[Paige Thomas]

I was thinking like

def List.SSubset
  {α : Type}
  (l₁ l₂ : List α) :
  Prop :=
  l₁ ⊆ l₂ ∧ ¬ l₂ ⊆ l₁

instance
  {α : Type}
  [DecidableEq α]
  (l₁ l₂ : List α) :
  Decidable (List.SSubset l₁ l₂) :=
  by
  unfold List.SSubset
  infer_instance

[Ruben Van de Velde]

What does a non-strict subset mean for lists?

[Ruben Van de Velde]

And possibly the answer is "nobody needed it enough yet"

[Aaron Liu]

l₁ ⊆ l₂ means l₁.toFinset ⊆ l₂.toFinset

[Antoine Chambert-Loir]

You don't care about repetitions?

[Aaron Liu]

That's what's in core

[Aaron Liu]

docs#List.instHasSubset

[Mario Carneiro]

The one that cares about repetitions is called "sublist", l₁ <+ l₂