def EuclidGeom.extractCollinear (expr : Q(Prop)) : Lean.MetaM (Option Lean.Expr)

Equations

• One or more equations did not get rendered due to their size.

def EuclidGeom.getCollinearDeclNames : Lean.Elab.Tactic.TacticM (List Lean.Name)

Equations

• One or more equations did not get rendered due to their size.

def EuclidGeom.perm_collinear : Lean.ParserDescr

Equations

• EuclidGeom.perm_collinear = Lean.ParserDescr.node `EuclidGeom.perm_collinear 1024 (Lean.ParserDescr.nonReservedSymbol "perm_collinear" false)

def EuclidGeom.evalPerm_collinear : Lean.Elab.Tactic.Tactic

Equations

• One or more equations did not get rendered due to their size.