lista konkat w z3
Czy istnieje sposób na połączenie dwóch list w z3? Podobny do operatora @ w ML? Myślałem o zdefiniowaniu go osobiście, ale nie sądzę, że z3 obsługuje rekurencyjne definicje funkcji, tj.
<code>define-fun concat ( (List l1) (List l2) List (ite (isNil l1) (l2) (concat (tail l1) (insert (head l1) l2)) ) ) </code>