How to write out variable declarations involving typeclasses

Stream: new members

[Marko Grdinić]

example {α χ : Type} [h : has_lt χ] [decidable_rel h.lt] (x : χ) (tree : rbmap χ α) : α :=
    match tree.find x with
    | some x := x
    | none := sorry
    end

I somehow managed to write the above out.

What I would like to do is write the above like...

variables {α χ : Type} [h : has_lt χ] [decidable_rel h.lt]

example (x : χ) (tree : rbmap χ α) : α :=
    match tree.find x with
    | some x := x
    | none := sorry
    end

...but it is not working for me. Is it possible to do this somehow?

Also as an aside, the Zulip allowed title length is too short. I do not even have room to put in an exclamation mark properly, let alone the full title.

[Marko Grdinić]

Alternatively, is there some other way to bundle types together with typeclasses?

[Floris van Doorn]

If you give a type class variable a name, you have to explicitly include it, using include h.

[Floris van Doorn]

This means that the hypothesis h (and therefore also χ) will be added to all declarations, even the ones that do not mention χ (you can use omit h to disable this).

[Mario Carneiro]

Regarding zulip title length, I am on a phone and I can only see "How to write out a variable decl...", even less from the main screen. So probably it is a bad idea to write too much in the title.