sym notation

Stream: general

[Yaël Dillies]

Is there a better notation to build concrete elements in sym?

import data.sym.basic

example (α : Type*) (a b c : α) :
  sym α 3 :=
a :: b :: c :: sym.nil

[Eric Wieser]

(docs#sym)

[Yaël Dillies]

Eric, the documentation bot :rofl:

[Kyle Miller]

No one's ever really wanted to before :smile:. I'd suggest using :: like that, though if you want there's also

example (α : Type*) (a b c : α) : sym α 3 := ⟨[a, b, c], rfl⟩

[Yaël Dillies]

Why is [, , ] notation not implemented for has_insert and has_nil?

[Yaël Dillies]

Oh wait, there's no has_nil!

[Kyle Miller]

I didn't check -- I'm pretty sure it's using the coercion from list there.

[Eric Wieser]

sym has no docs#has_insert anyway (nor can it, the types aren't right)

[Yaël Dillies]

Well, has_insert could well be heterogenous if we wanted to.

[Yakov Pechersky]

There's docs#has_emptyc

[Chris Hughes]

Can you use set notation {a, b, c} ?

[Eric Wieser]

No, that requires has_insert which can't apply here

[Eric Wieser]

@Yaël Dillies, you might have to fiddle with out_param to avoid confusing the elaborator

[Yaël Dillies]

Chris Hughes said:

Can you use set notation {a, b, c} ?

Didn't have much success doing so...

[Yaël Dillies]

Oh yeah, I'm not yet friend with the elaborator.

[Yury G. Kudryashov]

Why has_insert can't apply here? We can define it to mean cons.

[Eric Wieser]

Because it has signature insert : A → B → B which doesn't unify with cons.

[Yakov Pechersky]

import data.sym.basic

variable {α : Type*}

instance {n : ℕ} : has_coe_t (sym α n) (multiset α) :=
⟨subtype.val⟩

@[simp] lemma sym.coe_nil : ((sym.nil : sym α 0) : multiset α) = {} := rfl

@[simp] lemma sym.coe_cons {n : ℕ} (a : α) (s : sym α n) :
  ((sym.cons a s) : multiset α) = a ::ₘ (s : multiset α) :=
begin
  cases s,
  refl
end

instance [decidable_eq α] {n : ℕ} : decidable_eq (sym α n) := λ x y,
if h : (x : multiset α) = y
  then is_true (subtype.ext h)
  else is_false (λ H, h (congr_arg _ H))

notation `s[` l:(foldr `, ` (h t, sym.cons h t) sym.nil `]`) := l

-- for some reason, wouldn't work with subtype.decidable
example : s[1, 2, 3] = s[2, 1, 3] := dec_trivial