colGt in commands

Stream: lean4

[Jannis Limperg]

I'm trying to make a command that takes a list of identifiers, like this:

import Lean

elab withPosition("test") ns:(ppSpace colGt ident)+ : command =>
  Lean.logInfo m!"{ns}"

Afaiu, colGt should mean that this doesn't work:

test foo
bar

But it does and prints [foo, bar]. What am I doing wrong?

[Mario Carneiro]

colGt only works within the scope of a withPosition, that's why withPosition is a combinator and not just a 0-ary parser like colGt

[Mario Carneiro]

it asserts that the current parser column is gt the position of the nearest enclosing withPosition, if there is one

[Kyle Miller]

Interesting, the colGts/checkGolGts in the builtin commands don't do anything.

I wonder if a general fix should be to have the top-level command parser use withPosition. This would be like how it's by's responsibility to use withPosition, that way tactics don't each need to be wrapped in withPosition.

[Siddhartha Gadgil]

Mario Carneiro said:

colGt only works within the scope of a withPosition, that's why withPosition is a combinator and not just a 0-ary parser like colGt

I am trying to understand this. What is an example of withPosition that does work.

[Kyle Miller]

@Siddhartha Gadgil Here's an example where it does work:

example : True → True := by
  intro
h
  exact h

There's an error on h since it's not parsed as an argument to intro since colGt fails for that token. That h is being parsed as if it were a command. The by parser sets up withPosition for all the tactics that follow.

[Siddhartha Gadgil]

Thanks. What I was asking for was the parser definition which works

[Mario Carneiro]

syntax withPosition("test" (ppSpace colGt ident)+) : command

[Mario Carneiro]

you have to separate it from the elab_rules declaration though because the binding syntax doesn't support combinators like this