Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Binder syntax for vec_lambda

Email Gateway (May 02 2025 at 09:22):

From: Florian Haftmann <florian.haftmann@cit.tum.de>
In

https://foss.heptapod.net/isa-afp/afp-devel/-/blob/branch/default/thys/Fixed_Length_Vector/Fixed_Length_Vector.thy?ref_type=heads#L272

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

Last updated: May 06 2025 at 08:28 UTC