what is the name of `<;>`?

Stream: lean4

[Asei Inoue]

what is the name of <;>? (tactic combinator)

[Damiano Testa]

The parser is docs#Lean.Parser.Tactic.«tactic_<;>_», but I do not know its "name".

[Asei Inoue]

what should we call <;>...?

[Damiano Testa]

The linter that sees if it is unneeded is called linter.unnecessarySeqFocus, so maybe seqFocus is its name?

[David Renshaw]

When I needed a name for it in a recent video, I said "the pointy semicolon combinator" https://www.youtube.com/watch?v=KuxFWwwlEtc&t=375s

[David Renshaw]

... but that's kind of a mouthful

[David Thrane Christiansen]

"and in subgoals"?

[Floris van Doorn]

In Coq the equivalent is called Sequence

[Mario Carneiro]

I think it would be a bad idea to call it sequence because lean has sequential composition of tactics and this isn't it

[Mario Carneiro]

it's not clear to me whether coq does?

[Jannis Limperg]

Yeah, Coq uses tactic1. tactic2 for sequencing.

[David Thrane Christiansen]

What Lean calls ;, Coq calls .. What Lean calls <;>, Coq calls ;.

[David Thrane Christiansen]

<;> was called THEN in Edinburgh LCF

[Patrick Massot]

It used to be called ; in Lean 3 as well.

[Mario Carneiro]

Jannis Limperg said:

Yeah, Coq uses tactic1. tactic2 for sequencing.

This isn't actually a tactic operator, it's using two tactics. I don't know if coq has a tactic that has similar effect to tactic1. tactic2

[Mario Carneiro]

in lean this is spelled (tac1; tac2)

[Yann Herklotz]

I guess you can get similar behaviour in Coq using Local application of tactics: (tac1; [tac2|..]). And in Coq anything separated by . is called a sentence.