istep repeated arguments

Stream: general

[Eric Rodriguez]

why does istep have line0, col0, line and col? as far as I can see they're the same at all times

[Eric Rodriguez]

as in, the two lines are equal and so are the two cols

[Jason Rute]

I forgot, but I think I’ve found places they are different. Maybe ; or something like that. If no one knows I can look it up in some data I have.

[Mario Carneiro]

For tactics that are wrapped in solve1 because they involve a block somehow, the line/col denote the position of the close brace

[Eric Rodriguez]

what sort of tactic do you mean? I can't get it to happen with conv or suffices or anything like that

[Mario Carneiro]

I think by and begin should be able to do it, based on reading the code, but I haven't found an example yet

[Mario Carneiro]

there are a bunch of flags that all have to be set right for it to appear

[Mario Carneiro]

aha:

#check by { skip, [by { skip }] }

type mismatch at application
  has_bind.seq
    [has_bind.seq (tactic.save_info {line := 2, column := 22})
        (tactic.istep 2 22 2 22
           (has_bind.seq (tactic.save_info {line := 2, column := 22})
              (tactic.istep 2 22 2 29
                 (interactive.executor.execute_explicit tactic
                    (has_bind.seq
                       (has_bind.seq (tactic.save_info {line := 2, column := 22})
                          (has_bind.seq
                             (has_bind.seq (tactic.save_info {line := 2, column := 24})
                                (tactic.istep 2 24 2 24 tactic.interactive.skip))
                             (tactic.save_info {line := 2, column := 30})))
                       (tactic.save_info {line := 2, column := 29}))).solve1)).solve1)]

[Mario Carneiro]

the istep 2 22 2 29 is pointing at the { and } of the inner by { skip }

[Eric Rodriguez]

thanks so much!