+void Printer::toStreamCmdDefineFunctionRec(
+ std::ostream& out,
+ const std::vector<Node>& funcs,
+ const std::vector<Node>& lambdas) const
+{
+ std::vector<std::vector<Node>> formals;
+ std::vector<Node> formulas;
+ for (const Node& l : lambdas)
+ {
+ std::vector<Node> formalsVec;
+ Node formula;
+ if (l.getKind() == kind::LAMBDA)
+ {
+ formalsVec.insert(formalsVec.end(), l[0].begin(), l[0].end());
+ formula = l[1];
+ }
+ else
+ {
+ formula = l;
+ }
+ formals.emplace_back(formalsVec);
+ formulas.emplace_back(formula);
+ }
+ toStreamCmdDefineFunctionRec(out, funcs, formals, formulas);
+}
+