synth DecidableEq

Stream: new members

[Xiyu Zhai]

Hi, everyone. In the following code in Lean4, I want to make Expr to be DecidableEq so that ExprWrapper can be derived to be such. But all my attempts failed. Expr can be derived to be DecidableEq because it contains a list of Expr.

inductive Expr
  | Variable
  | Opn (opds : List Expr)
  -- deriving DecidableEq

def Expr.deq (a b : Expr) : Decidable (a = b) := sorry
-- instance : DecidableEq Expr := by sorry

structure ExprWrapper where
  expr : Expr
  deriving DecidableEq

Thanks a lot!