Lean4
/-- The line between two points, as an affine subspace. -/
@[term_parser 1000]
public meta def «termLine[_,_,_]» : Lean.ParserDescr✝ :=
ParserDescr.node✝ `«termLine[_,_,_]» 1024
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "line[") (ParserDescr.cat✝ `term 0))
(ParserDescr.symbol✝ ", "))
(ParserDescr.cat✝ `term 0))
(ParserDescr.symbol✝ ", "))
(ParserDescr.cat✝ `term 0))
(ParserDescr.symbol✝ "]"))