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›

Last updated: Jul 15 2022 at 23:21 UTC