English
There exists a decidable equality on L.Term α provided DecidableEq α and DecidableEq for all function arities L.Functions n; equality is decided by structural recursion on the term.
Русский
Существует разрешимое равенство на L.Term α при условии DecidableEq α и DecidableEq для всех аритетов функций; равенство определяется по структурному разбору терма.
LaTeX
$$$ \operatorname{DecidableEq}(L.\text{Term } \alpha) \text{ assuming } [\operatorname{DecidableEq} \alpha] \ \text{and } (\forall n, \operatorname{DecidableEq}(L.\text{Functions } n)).$$$
Lean4
instance instDecidableEq [DecidableEq α] [∀ n, DecidableEq (L.Functions n)] : DecidableEq (L.Term α)
| .var a, .var b => decidable_of_iff (a = b) <| by simp
| @Term.func _ _ m f xs, @Term.func _ _ n g ys =>
if h : m = n then
letI : DecidableEq (L.Term α) := instDecidableEq
decidable_of_iff (f = h ▸ g ∧ ∀ i : Fin m, xs i = ys (Fin.cast h i)) <|
by
subst h
simp [funext_iff]
else .isFalse <| by simp [h]
| .var _, .func _ _ | .func _ _, .var _ => .isFalse <| by simp
