Mutually required notation

Stream: lean4

[Zach Battleman]

Is there a way to setup a syntax where two disjoint pieces are optional such as with ?, but if one occurs the other must occur as well? For example something like syntax ("foo " term)? "baz " term ("bar " term)? : term where if either the foo term or bar term appears, the other must appear or it would be considered invalid?

Also, as a quick aside I'm trying to log in an elaborator and nothing is appearing. For example, I updated Elab.Term.elabForIn to always include a log, but it is not printing anything when I eval a for loop. I suspect this has to do with files not getting rebuilt properly, but lake build and refresh file dependencies don't seem to work. Any ideas on this? Thanks!

[Zach Battleman]

Also, in an elaborator, why can I not provide names to optional arguments? For example, I can do
elab "for'" itr:ident " in " ..., but I cannot do elab "for'" (itr:ident ")? in" ...

[Mario Carneiro]

for your last question, you can do elab "for'" itr:(ident)? " in " ...

[Zach Battleman]

ah great thanks! Sorry last thing, in an elab, how do I get the equivalent of the option type argument as seen here

@[term_elab myterm1]
def myTerm1Impl : TermElab := fun stx type? => sorry

Ah I think the <= t => notation does it?