def Lean.TSyntax.freshIdent {m : Type → Type} [Monad m] [MonadQuotation m] : m (TSyntax `ident)

Equations

• Lean.TSyntax.freshIdent = do let name ← Lean.Elab.Term.mkFreshBinderName pure { raw := (Lean.mkIdent name).raw }

def LO.FirstOrder.Semiformula.nestFormulae {L : Language} {ξ : Type u_1} {n m : ℕ} (φ : Semiformula L ξ n) (Ψ : Fin n → Semiformula L ξ (m + 1)) : Semiformula L ξ m

Equations

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

def LO.FirstOrder.Semiformula.nestFormulaeFunc {L : Language} {ξ : Type u_1} {n m : ℕ} (φ : Semiformula L ξ (n + 1)) (Ψ : Fin n → Semiformula L ξ (m + 1)) : Semiformula L ξ (m + 1)

Equations

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

theorem LO.FirstOrder.Semiformula.eval_nestFormulae {L : Language} {ξ : Type u_1} {M : Type u_2} [s : Structure L M] {f : ξ → M} {n m : ℕ} {e : Fin m → M} {φ : Semiformula L ξ n} {Ψ : Fin n → Semiformula L ξ (m + 1)} : (Eval e f) (φ.nestFormulae Ψ) ↔ ∀ (v : Fin n → M), (∀ (i : Fin n), (Eval (v i :> e) f) (Ψ i)) → (Eval v f) φ

@[simp]

theorem LO.FirstOrder.Semiformula.eval_nestFormulae₀ {L : Language} {ξ : Type u_1} {M : Type u_2} [s : Structure L M] {f : ξ → M} {n✝ : ℕ} {e : Fin n✝ → M} {φ : Semiformula L ξ 0} : (Eval e f) (φ.nestFormulae ![]) ↔ (Eval ![] f) φ

@[simp]

theorem LO.FirstOrder.Semiformula.eval_nestFormulae₁ {L : Language} {ξ : Type u_1} {M : Type u_2} [s : Structure L M] {f : ξ → M} {m : ℕ} {e : Fin m → M} {φ : Semiformula L ξ 1} {ψ : Semiformula L ξ (m + 1)} : (Eval e f) (φ.nestFormulae ![ψ]) ↔ ∀ (x : M), (Eval (x :> e) f) ψ → (Eval ![x] f) φ

@[simp]

theorem LO.FirstOrder.Semiformula.eval_nestFormulae₂ {L : Language} {ξ : Type u_1} {M : Type u_2} [s : Structure L M] {f : ξ → M} {m : ℕ} {e : Fin m → M} {φ : Semiformula L ξ 2} {ψ₁ ψ₂ : Semiformula L ξ (m + 1)} : (Eval e f) (φ.nestFormulae ![ψ₁, ψ₂]) ↔ ∀ (x₁ : M), (Eval (x₁ :> e) f) ψ₁ → ∀ (x₂ : M), (Eval (x₂ :> e) f) ψ₂ → (Eval ![x₁, x₂] f) φ

@[simp]

theorem LO.FirstOrder.Semiformula.eval_nestFormulae₃ {L : Language} {ξ : Type u_1} {M : Type u_2} [s : Structure L M] {f : ξ → M} {m : ℕ} {e : Fin m → M} {φ : Semiformula L ξ 3} {ψ₁ ψ₂ ψ₃ : Semiformula L ξ (m + 1)} : (Eval e f) (φ.nestFormulae ![ψ₁, ψ₂, ψ₃]) ↔ ∀ (x₁ : M), (Eval (x₁ :> e) f) ψ₁ → ∀ (x₂ : M), (Eval (x₂ :> e) f) ψ₂ → ∀ (x₃ : M), (Eval (x₃ :> e) f) ψ₃ → (Eval ![x₁, x₂, x₃] f) φ

@[simp]

theorem LO.FirstOrder.Semiformula.eval_nestFormulae₄ {L : Language} {ξ : Type u_1} {M : Type u_2} [s : Structure L M] {f : ξ → M} {m : ℕ} {e : Fin m → M} {φ : Semiformula L ξ 4} {ψ₁ ψ₂ ψ₃ ψ₄ : Semiformula L ξ (m + 1)} : (Eval e f) (φ.nestFormulae ![ψ₁, ψ₂, ψ₃, ψ₄]) ↔ ∀ (x₁ : M), (Eval (x₁ :> e) f) ψ₁ → ∀ (x₂ : M), (Eval (x₂ :> e) f) ψ₂ → ∀ (x₃ : M), (Eval (x₃ :> e) f) ψ₃ → ∀ (x₄ : M), (Eval (x₄ :> e) f) ψ₄ → (Eval ![x₁, x₂, x₃, x₄] f) φ

theorem LO.FirstOrder.Semiformula.eval_nestFormulaeFunc {L : Language} {ξ : Type u_1} {M : Type u_2} [s : Structure L M] {f : ξ → M} {n m : ℕ} {z : M} {e : Fin m → M} {φ : Semiformula L ξ (n + 1)} {Ψ : Fin n → Semiformula L ξ (m + 1)} : (Eval (z :> e) f) (φ.nestFormulaeFunc Ψ) ↔ ∀ (v : Fin n → M), (∀ (i : Fin n), (Eval (v i :> e) f) (Ψ i)) → (Eval (z :> v) f) φ

@[simp]

theorem LO.FirstOrder.Semiformula.eval_nestFormulaeFunc₀ {L : Language} {ξ : Type u_1} {M : Type u_2} [s : Structure L M] {f : ξ → M} {z : M} {n✝ : ℕ} {e : Fin n✝ → M} {φ : Semiformula L ξ 1} : (Eval (z :> e) f) (φ.nestFormulaeFunc ![]) ↔ (Eval ![z] f) φ

@[simp]

theorem LO.FirstOrder.Semiformula.eval_nestFormulaeFunc₁ {L : Language} {ξ : Type u_1} {M : Type u_2} [s : Structure L M] {f : ξ → M} {m : ℕ} {z : M} {e : Fin m → M} {φ : Semiformula L ξ 2} {ψ : Semiformula L ξ (m + 1)} : (Eval (z :> e) f) (φ.nestFormulaeFunc ![ψ]) ↔ ∀ (x : M), (Eval (x :> e) f) ψ → (Eval ![z, x] f) φ

@[simp]

theorem LO.FirstOrder.Semiformula.eval_nestFormulaeFunc₂ {L : Language} {ξ : Type u_1} {M : Type u_2} [s : Structure L M] {f : ξ → M} {m : ℕ} {z : M} {e : Fin m → M} {φ : Semiformula L ξ 3} {ψ₁ ψ₂ : Semiformula L ξ (m + 1)} : (Eval (z :> e) f) (φ.nestFormulaeFunc ![ψ₁, ψ₂]) ↔ ∀ (x₁ : M), (Eval (x₁ :> e) f) ψ₁ → ∀ (x₂ : M), (Eval (x₂ :> e) f) ψ₂ → (Eval ![z, x₁, x₂] f) φ

@[simp]

theorem LO.FirstOrder.Semiformula.eval_nestFormulaeFunc₃ {L : Language} {ξ : Type u_1} {M : Type u_2} [s : Structure L M] {f : ξ → M} {m : ℕ} {z : M} {e : Fin m → M} {φ : Semiformula L ξ 4} {ψ₁ ψ₂ ψ₃ : Semiformula L ξ (m + 1)} : (Eval (z :> e) f) (φ.nestFormulaeFunc ![ψ₁, ψ₂, ψ₃]) ↔ ∀ (x₁ : M), (Eval (x₁ :> e) f) ψ₁ → ∀ (x₂ : M), (Eval (x₂ :> e) f) ψ₂ → ∀ (x₃ : M), (Eval (x₃ :> e) f) ψ₃ → (Eval ![z, x₁, x₂, x₃] f) φ

@[simp]

theorem LO.FirstOrder.Semiformula.eval_nestFormulaeFunc₄ {L : Language} {ξ : Type u_1} {M : Type u_2} [s : Structure L M] {f : ξ → M} {m : ℕ} {z : M} {e : Fin m → M} {φ : Semiformula L ξ 5} {ψ₁ ψ₂ ψ₃ ψ₄ : Semiformula L ξ (m + 1)} : (Eval (z :> e) f) (φ.nestFormulaeFunc ![ψ₁, ψ₂, ψ₃, ψ₄]) ↔ ∀ (x₁ : M), (Eval (x₁ :> e) f) ψ₁ → ∀ (x₂ : M), (Eval (x₂ :> e) f) ψ₂ → ∀ (x₃ : M), (Eval (x₃ :> e) f) ψ₃ → ∀ (x₄ : M), (Eval (x₄ :> e) f) ψ₄ → (Eval ![z, x₁, x₂, x₃, x₄] f) φ

@[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

(Literal) Notation for terms

def Lean.Parser.Category.first_order_term : 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.first_order.quote_type.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.first_order.quote_type : Category

Equations

• Lean.Parser.Category.first_order.quote_type = { }

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

Equations

• LO.FirstOrder.BinderNotation.quote_typeLit = Lean.ParserDescr.node `LO.FirstOrder.BinderNotation.quote_typeLit 1024 (Lean.ParserDescr.symbol "lit")

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

Equations

• LO.FirstOrder.BinderNotation.quote_typeFaf = Lean.ParserDescr.node `LO.FirstOrder.BinderNotation.quote_typeFaf 1024 (Lean.ParserDescr.symbol "faf")

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.unexpandNumeral : Lean.PrettyPrinter.Unexpander

Equations

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

Notation for formulae

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 : 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_formulaOf_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

• 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.

Notation for formula as term

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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