mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

Added "λ" pretty printing to python (#7320)

Browse source
This commit is contained in:
Philip Zucker 2024-07-31 11:14:16 -04:00 committed by GitHub
parent 0c16d34eb0
commit e7382d6ff9
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/api/python/z3/z3printer.py
View file

@ -1412,8 +1412,10 @@ class HTMLFormatter(Formatter):
ys_pp = group(seq(ys)) ys_pp = group(seq(ys))
if a.is_forall(): if a.is_forall():
header = "∀" header = "∀"
else: elif a.is_exists():
header = "∃" header = "∃"
else:
header = "λ"
return group(compose(to_format(header, 1), return group(compose(to_format(header, 1),
indent(1, compose(ys_pp, to_format(" :"), line_break(), body_pp)))) indent(1, compose(ys_pp, to_format(" :"), line_break(), body_pp))))