Email Gateway (Aug 18 2022 at 13:45): Email Gateway (Aug 18 2022 at 13:45):From: Dennis Walter <dennis.walter@gmail.com>
Hi,
I have a question concerning concrete syntax for record updates. In
the context of a record R
record R = f :: nat
I can write
term "x(| f := 1 |)"
This gets displayed as
"x(| f := 1 |)"
:: "'a R_scheme"
which is what I'd expect. However, updating an application
term "(g x)(| f := 1 |)"
gets displayed as
"f_update (%_. 1) (g x)"
:: "'a R_scheme"
I understand that both "g x"-terms are internally equal and that it's
just a matter of pretty printing. However, I don't understand why the
syntax translation machinery fails to pretty print the application.
Can somebody explain it to me?
Thanks,
Dennis
Last updated: May 03 2024 at 04:19 UTC