| 565 | } |
| 566 | |
| 567 | bool expr::isLambda(expr &body) const { |
| 568 | C(); |
| 569 | if (Z3_is_lambda(ctx(), ast())) { |
| 570 | assert(Z3_get_quantifier_num_bound(ctx(), ast()) == 1); |
| 571 | body = Z3_get_quantifier_body(ctx(), ast()); |
| 572 | return true; |
| 573 | } |
| 574 | return false; |
| 575 | } |
| 576 | |
| 577 | expr expr::lambdaIdxType() const { |
| 578 | C(); |