список конкат в z3
Есть ли способ объединить два списка в z3? Похоже на оператор @ в ML? Я думал о том, чтобы определить это сам, но я не думаю, что z3 поддерживает определения рекурсивных функций, т.е.
<code>define-fun concat ( (List l1) (List l2) List (ite (isNil l1) (l2) (concat (tail l1) (insert (head l1) l2)) ) ) </code>