fact: Fixpoint encode_algT F (f : algterm F) : GenTree.tree (F + const) := let T_ isbin := if isbin then binOp else unOp in match f with | Base x => GenTree.Leaf (inl x) | Const c => GenTree.Leaf (inr c) | UnOp u f1 => GenTree.Node (pickle (inl u : unOp + binOp)) [:: encode_algT f1] | BinOp b f1 f2 => GenTree.Node (pickle (inr b : unOp + binOp)) [:: encode_algT f1; encode_algT f2] end.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field polyrcf) Abel(various classic_ext map_gal algR) Abel(char0 cyclotomic_ext real_closed_ext)