fact: Fixpoint decode_algT F (t : GenTree.tree (F + const)) : algterm F := match t with | GenTree.Leaf (inl x) => Base x | GenTree.Leaf (inr c) => Const c | GenTree.Node n fs => match locked (unpickle n), fs with | Some (inl u), f1 :: _ => UnOp u (decode_algT f1) | Some (inr b), f1 :: f2 :: _ => BinOp b (decode_algT f1) (decode_algT f2) | _, _ => Const Zero end 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)