4cf3c0ae67
This PR adds the `reduceBEq` and `reduceOrd` simprocs. They rewrite occurrences of `_ == _` resp. `Ord.compare _ _` if both arguments are constructors and the corresponding instance has been marked with `@[method_specs]` (introduced in #10302), which now by default is the case for derived instances.
11 lines
282 B
Text
11 lines
282 B
Text
-- set_option trace.Elab.Deriving.lawfulBEq true
|
||
|
||
inductive L (α : Type u) where
|
||
| nil : L α
|
||
| cons : α → L α → L α
|
||
deriving BEq
|
||
|
||
example {n m : Nat} (h : n = m) :
|
||
(L.cons n (L.nil : L Nat) == L.cons m (L.nil : L Nat)) = true := by
|
||
simp [reduceBEq]
|
||
assumption
|