Stream: Beginner Questions

Topic: ✔ Record accessor subscript

Robert Soeldner (Apr 22 2022 at 11:43):

Is it possible to define a syntax for using a subscribed identifier var with record accessors? E.g.

record Obj =
  valid :: bool

lemma ‹valid\<^sub>G›

instead of

lemma ‹valid G›

Kevin Kappelmann (Apr 23 2022 at 16:34):

You could use bsub and esub:

notation valid ("valid⇘_⇙")

term "valid⇘G⇙"

Notification Bot (Apr 23 2022 at 16:49):

Robert Soeldner has marked this topic as resolved.

Last updated: Sep 28 2026 at 16:33 UTC