From d249c0fd7d2c49056e9c5f3ded7f83ebfc74a0c2 Mon Sep 17 00:00:00 2001 From: Philip Zucker Date: Wed, 31 Jul 2024 09:16:19 -0400 Subject: [PATCH] Added "λ" pretty printing to python --- src/api/python/z3/z3printer.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/api/python/z3/z3printer.py b/src/api/python/z3/z3printer.py index 2da5f89da..d7ee17f4a 100644 --- a/src/api/python/z3/z3printer.py +++ b/src/api/python/z3/z3printer.py @@ -1412,8 +1412,10 @@ class HTMLFormatter(Formatter): ys_pp = group(seq(ys)) if a.is_forall(): header = "∀" - else: + elif a.is_exists(): header = "∃" + else: + header = "λ" return group(compose(to_format(header, 1), indent(1, compose(ys_pp, to_format(" :"), line_break(), body_pp))))