@[reducible, inline]

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

Equations

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

@[simp]

theorem LO.FirstOrder.BinderNotation.finSuccItr_one {n : ℕ} {x : Fin n} : LO.FirstOrder.BinderNotation.finSuccItr x 1 = x.succ

@[simp]

theorem LO.FirstOrder.BinderNotation.finSuccItr_two {n : ℕ} {x : Fin n} : LO.FirstOrder.BinderNotation.finSuccItr x 2 = x.succ.succ

def Lean.Parser.Category.first_order_term : Lean.Parser.Category

Equations

• Lean.Parser.Category.first_order_term = { }

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Parser.Category.first_order_formula : Lean.Parser.Category

Equations

• Lean.Parser.Category.first_order_formula = { }

def LO.FirstOrder.BinderNotation.«term⤫formula[_|_|_]» : Lean.ParserDescr

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def LO.FirstOrder.BinderNotation.«first_order_formula_≮_» : Lean.ParserDescr

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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