Zulip Chat Archive

Stream: general

Topic: istep repeated arguments


Eric Rodriguez (Aug 02 2021 at 19:04):

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

Eric Rodriguez (Aug 02 2021 at 19:04):

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

Jason Rute (Aug 02 2021 at 22:18):

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 (Aug 02 2021 at 22:22):

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 (Aug 02 2021 at 22:38):

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

Mario Carneiro (Aug 02 2021 at 22:38):

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 (Aug 02 2021 at 22:39):

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

Mario Carneiro (Aug 02 2021 at 22:46):

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 (Aug 02 2021 at 22:47):

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

Eric Rodriguez (Aug 02 2021 at 22:49):

thanks so much!


Last updated: Dec 20 2023 at 11:08 UTC