BinderNotation

@[reducible, inline]

abbrev LO.FirstOrder.BinderNotation.finSuccItr {n : ℕ} (i : Fin n) (m : ℕ) : Fin (n + m)

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.BinderNotation.finSuccItr i 0 = i
• LO.FirstOrder.BinderNotation.finSuccItr i m.succ = (LO.FirstOrder.BinderNotation.finSuccItr i m).succ

def Lean.Parser.Category.firstOrderTerm : Category

Imported declaration from the Incompleteness formalization.

Equations

• Lean.Parser.Category.firstOrderTerm = { }

def LO.FirstOrder.BinderNotation.firstOrderTerm.quot : Lean.ParserDescr

Equations

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

def LO.FirstOrder.BinderNotation.«termFoTerm[_|_|_]» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderTerm(_)» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.firstOrderTerm_ : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.BinderNotation.firstOrderTerm_ = Lean.ParserDescr.node `LO.FirstOrder.BinderNotation.firstOrderTerm_ 1024 (Lean.ParserDescr.const `ident)

def LO.FirstOrder.BinderNotation.«firstOrderTerm#_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderTerm&_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderTerm!__⋯» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.firstOrderTerm!!_ : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderTerm.!__⋯» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderTerm.!!_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.firstOrderTerm__1 : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.BinderNotation.firstOrderTerm__1 = Lean.ParserDescr.node `LO.FirstOrder.BinderNotation.firstOrderTerm__1 1022 (Lean.ParserDescr.const `num)

def LO.FirstOrder.BinderNotation.«firstOrderTerm↑_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderTerm⋆» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.BinderNotation.«firstOrderTerm⋆» = Lean.ParserDescr.node `LO.FirstOrder.BinderNotation.«firstOrderTerm⋆» 1024 (Lean.ParserDescr.symbol "⋆")

def LO.FirstOrder.BinderNotation.«firstOrderTerm_+_» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderTerm_*_» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderTerm_^_» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderTerm_^'_» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderTerm_²» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.BinderNotation.«firstOrderTerm_²» = Lean.ParserDescr.trailingNode `LO.FirstOrder.BinderNotation.«firstOrderTerm_²» 1024 0 (Lean.ParserDescr.symbol "²")

def LO.FirstOrder.BinderNotation.«firstOrderTerm_³» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.BinderNotation.«firstOrderTerm_³» = Lean.ParserDescr.trailingNode `LO.FirstOrder.BinderNotation.«firstOrderTerm_³» 1024 0 (Lean.ParserDescr.symbol "³")

def LO.FirstOrder.BinderNotation.«firstOrderTerm_⁴» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.BinderNotation.«firstOrderTerm_⁴» = Lean.ParserDescr.trailingNode `LO.FirstOrder.BinderNotation.«firstOrderTerm_⁴» 1024 0 (Lean.ParserDescr.symbol "⁴")

def LO.FirstOrder.BinderNotation.«firstOrderTerm⌜_⌝» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.firstOrderTermExp_ : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«term‘_’» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«term‘_|_’» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«term‘_._’» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.unexpsnderNatLit : Lean.PrettyPrinter.Unexpander

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.unexpsnderOperatorConst : Lean.PrettyPrinter.Unexpander

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.unexpsnderAdd : Lean.PrettyPrinter.Unexpander

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.unexpsnderMul : Lean.PrettyPrinter.Unexpander

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.unexpandFuncArith : Lean.PrettyPrinter.Unexpander

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.unexpandNumeral : Lean.PrettyPrinter.Unexpander

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.firstOrderFormula.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.firstOrderFormula : Category

Imported declaration from the Incompleteness formalization.

Equations

• Lean.Parser.Category.firstOrderFormula = { }

def LO.FirstOrder.BinderNotation.«termFoFormula[_|_|_]» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderFormula(_)» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderFormula!__⋯» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.firstOrderFormula!!_ : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderFormula.!__⋯» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderFormula.!!_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderFormula⊤» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.BinderNotation.«firstOrderFormula⊤» = Lean.ParserDescr.node `LO.FirstOrder.BinderNotation.«firstOrderFormula⊤» 1024 (Lean.ParserDescr.symbol "⊤")

def LO.FirstOrder.BinderNotation.«firstOrderFormula⊥» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.BinderNotation.«firstOrderFormula⊥» = Lean.ParserDescr.node `LO.FirstOrder.BinderNotation.«firstOrderFormula⊥» 1024 (Lean.ParserDescr.symbol "⊥")

def LO.FirstOrder.BinderNotation.«firstOrderFormula_∧_» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderFormula_∨_» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderFormula¬_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderFormula_→_» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderFormula_↔_» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderFormula⋀_,_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderFormula⋁_,_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderFormula⋀_<_,_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderFormula⋁_<_,_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderFormula∀_,_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderFormula∃_,_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderFormula∀'_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderFormula∃'_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderFormula∀[_]_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderFormula∃[_]_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«term“_|_”» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«term“_._”» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«term“_”» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderFormula_=_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderFormula_<_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderFormula_>_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderFormula_≤_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderFormula_≥_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderFormula_∈_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderFormula_∋_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderFormula_≠_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderFormula_</_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderFormula_≰_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderFormula_∉_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderFormula∀_<_,_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderFormula∀_≤_,_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderFormula∀_∈_,_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderFormula∃_<_,_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderFormula∃_≤_,_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.«firstOrderFormula∃_∈_,_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.unexpsnderEq : Lean.PrettyPrinter.Unexpander

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.unexpsnderLe : Lean.PrettyPrinter.Unexpander

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.unexpandAnd : Lean.PrettyPrinter.Unexpander

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.unexpandOr : Lean.PrettyPrinter.Unexpander

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.unexpandNeg : Lean.PrettyPrinter.Unexpander

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.unexpandUniv : Lean.PrettyPrinter.Unexpander

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.unexpandEx : Lean.PrettyPrinter.Unexpander

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.unexpandBall : Lean.PrettyPrinter.Unexpander

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.unexpandBex : Lean.PrettyPrinter.Unexpander

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.unexpandArrow : Lean.PrettyPrinter.Unexpander

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.unexpandIff : Lean.PrettyPrinter.Unexpander

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.BinderNotation.unexpandOpArith : Lean.PrettyPrinter.Unexpander

Imported declaration from the Incompleteness formalization.

Equations

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