blob: 1e93a2c10b00dd265c2a0787245f4b4f084821b1 (
plain)
1
2
3
4
5
6
|
From mathcomp Require Import all_ssreflect.
Inductive tree := Node { children : seq tree }.
Fixpoint eq_tree (x y : tree) {struct x} : bool :=
all2 eq_tree (children x) (children y).
|