def EuclideanGeometry.«termℝ^_» : Lean.ParserDescr

Equations

• EuclideanGeometry.«termℝ^_» = Lean.ParserDescr.node `EuclideanGeometry.«termℝ^_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "ℝ^") (Lean.ParserDescr.cat `term 65))