Failed to synthesize instance Decidable

Stream: new members

[nrs]

inductive mTerm where
  | var : String -> mTerm
  | other : mTerm

def func (t: mTerm) (s: String) : Option String :=
  match t with
  | mTerm.var vs => if vs = s then some vs else none
  | _ => none

The above code produces: failed to synthesize instance Decidable (vs = s). What does this mean?

[Adam Topaz]

In order to use if p then ... else ... the proposition p needs to be decidable. In this case, you need decidable equality on mTerm. If you write

inductive mTerm where
  | var : String -> mTerm
  | other : mTerm
deriving DecidableEq

then you should be good to go

[nrs]

Adam Topaz said:

In order to use if p then ... else ... the proposition p needs to be decidable. In this case, you need decidable equality on mTerm. If you write

inductive mTerm where
  | var : String -> mTerm
  | other : mTerm
deriving DecidableEq

then you should be good to go

that worked, thank you! by any chance, would you know where I could read about what deriving DecidableEq does?

[Adam Topaz]

this derives a decidable eq isntance for your type. You may be better off reading the documentation around docs#DecidableEq

[Adam Topaz]

if you really want to see how it's derived, you could look at the deriving handler, but getting its name would require some digging

[nrs]

Adam Topaz said:

if you really want to see how it's derived, you could look at the deriving handler, but getting its name would require some digging

noted, thanks for taking the time!

[Adam Topaz]

It seems that the code that derives decidable eqs can be found in this file: https://github.com/leanprover/lean4/blob/ec3042d94bd11a42430f9e14d39e26b1f880f99b/src/Lean/Elab/Deriving/DecEq.lean

[Kyle Miller]

deriving clauses invoke so-called deriving handlers, and these try to automatically synthesize code to implement a given typeclass, if possible.

Decidable p is a fancy Bool whose values contain a proof or disproof of p. So, just think about how you'd write a Bool-valued equality procedure for mTerm, and then to elevate it to a DecidableEq mTerm instance it needs to also come up with proofs for why each true or false it returns is correct. Luckily this boilerplate can be automated with deriving DecidableEq most of the time.

[Kyle Miller]

(note that DecidableEq X is an abbreviation for fun (x y : X) => Decidable (x = y))

[nrs]

I'll be mulling over your descriptions and the definitions and reading the code, thank you very much to both for taking the time!!