Decidable equality

Stream: lean4

[Pavel Shuhray]

Hi

universe u
constant T : Type u

I want to say "T is a fixed type with decidable equality". How can I do it? Please, give a complete solution.

[Mario Carneiro]

it depends on what you mean by fixed. Usually variable (T : Type u) [DecidableEq T] is sufficient

[Marcus Rossel]

Pavel Shuhray said:

I want to say "T is a fixed type with decidable equality". How can I do it? Please, give a complete solution.

I think I've tried to do the same thing before: Opaque type with interface
Adapting that approach to your case would yield:

private constant _T : Σ T : Type _, DecidableEq T := Sigma.mk Unit inferInstance

def T : Type _ := _T.fst
instance : DecidableEq T := _T.snd

(But I think you should really consider Mario's version unless you have strong reasons to use a constant.)

[Pavel Shuhray]

Are there "parameters" in Lean4?

[Henrik Böving]

You'll have to explain what you mean by that

[Pavel Shuhray]

In Lean3 I can write

parameter x : A

[Horatiu Cheval]

No, see this thread: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/parameter

[Horatiu Cheval]

But Sebastian also gives there a way users can implement parameter themselves.