mkNullNode

Stream: lean4

[Marcus Rossel]

I'm pretty sure this used to work:

macro "mwe" : command => do
  return mkNullNode #[]

But on the current nightly I get:

application type mismatch
  pure (mkNullNode #[])
argument
  mkNullNode #[]
has type
  Syntax : Type
but is expected to have type
  TSyntax `command : Type

What is the proper way of combining multiple Commands into a single command now?

(Cf. an answer by Gabriel on this topic.)

[Mario Carneiro]

you can just do return ⟨mkNullNode⟩

[Sebastian Ullrich]

@Gabriel Ebner @Mario Carneiro Do you see a nice solution here? I don't think we want to introduce a commands category just for that. For tactics we already have ($tac1; $tac2), perhaps we should allow section (or some new syntax) to parse contained commands eagerly when inside a quotation as in

`(command| section
  $cmd1
  $cmd2)

[Mario Carneiro]

why not just invent some kind of grouping syntax for commands?

[Mario Carneiro]

we already have mutual, so a grouping syntax wouldn't be any more complicated than that

[Mario Carneiro]

I think meta if also frequently needs command groups

[Mario Carneiro]

How about:

section name? {
 $cmd1
 $cmd2
}

[Mario Carneiro]

which behaves exactly like section ... end except it is a single command

[Sebastian Ullrich]

I don't see an advantage over my suggestion tbh

[Mario Carneiro]

having syntax that is only valid in quotations is not nice

[Mario Carneiro]

also your syntax has no terminator

[Mario Carneiro]

To be clear, users would also be able to write section foo { def bar := 1 }

[Sebastian Ullrich]

But the syntax is just as valid outside! That the following commands are not technically part of the section syntax is an implementation detail, people certainly think of them being part of the section.

[Mario Carneiro]

I can imagine some people will prefer that style, although it remains to be seen what kind of side effects arise from it being a single command

[Sebastian Ullrich]

Mario Carneiro said:

also your syntax has no terminator

Well end would be the obvious one

[Sebastian Ullrich]

Just not quite as obvious to parse, but we should manage :)

[Mario Carneiro]

I think it is simpler overall not to special case quotations and just have a general purpose grouping syntax

[Mario Carneiro]

section is not a grouping syntax in that sense, at least currently

[Mario Carneiro]

I'm assuming that ( is not an option