Email Gateway (May 02 2025 at 09:22): Email Gateway (May 02 2025 at 09:22):From: Florian Haftmann <florian.haftmann@cit.tum.de>
In
there is
lift_definition vec_lambda :: ‹('b :: index ⇒ 'a) ⇒ 'a ^ 'b› (binder ‹χ› 10)
is ‹λf. map f indexes› by simp
The term ‹vec_lambda (λv. f v i)› then prints as ‹χv. f v i›, which does
not parse again, but ‹χ v. f v i› does.
The cause might be that χ and v share the same lexical category.
What to do here? My first idea would be to change the syntax to (binder
‹χ › 10) but there might be more behind it.
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Email Gateway (May 21 2025 at 09:15):From: Makarius <makarius@sketis.net>
On 02/05/2025 11:21, Florian Haftmann wrote:
In
https://foss.heptapod.net/isa-afp/afp-devel/-/blob/branch/default/thys/
Fixed_Length_Vector/Fixed_Length_Vector.thy?ref_type=heads#L272there is
lift_definition vec_lambda :: ‹('b :: index ⇒ 'a) ⇒ 'a ^ 'b› (binder ‹χ› 10)
is ‹λf. map f indexes› by simpThe term ‹vec_lambda (λv. f v i)› then prints as ‹χv. f v i›, which does not
parse again, but ‹χ v. f v i› does.The cause might be that χ and v share the same lexical category.
The problem is indeed that greek and latin letters may be freely mixed to form
an identifier. That issue was swept under the carpet many decades ago by
treating \<lambda> as a non-letter. So it happens to work there, but in
generality it doesn't.
The usual workaround in library theories is to use an extra space like this:
My first idea would be to change the syntax to (binder ‹χ ›
10) but there might be more behind it.
I have no better idea right now. It falls into the category "our bad habits
have become best practices".
Makarius
Last updated: May 30 2025 at 04:27 UTC