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 FFL.FirstOrder.Semiformula.nestFormulae {L : Language} {ξ : Type u_1} {n m : ℕ} (φ : Semiformula L ξ n) (Ψ : Fin n → Semiformula L ξ (m + 1)) : Semiformula L ξ m

nestFormulae φ(x₁,…,xₙ) ![Ψ₁(x₁,y₁,…,yₘ), …, Ψₙ(xₙ,y₁,…,yₘ)] is the formula ∀ x₁, …, xₙ ((Ψ₁(x₁,y₁,…,yₘ) ∧ … ∧ Ψₙ(xₙ,y₁,…,yₘ)) → φ(x₁,…,xₙ)).

Here, each formula Ψᵢ has m + 1 bound variables, one for expressing a predicate of an xᵢ, and m remaining ones. In the resulting formula, the bound variables are the m remaining bound variables, while all of the original n bound variables of φ get bounded to a ∀ quantifier.

Intuitively, nestFormulae gives R(f₁(y₁,…,yₘ), …, fₙ(y₁,…,yₘ)), the result of substituting functions f₁, … fₙ into a relation R, using the defining formulae of their graphs (xᵢ = fᵢ(y₁,…,yₘ) iff Ψᵢ(xᵢ,y₁,…,yₘ), and R(x₁,…,xₙ) iff φ(x₁,…,xₙ)).

Equations

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

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

nestFormulaeFunc φ(x,x₁,…,xₙ) ![Ψ₁(x₁,y₁,…,yₘ), …, Ψₙ(xₙ,y₁,…,yₘ)] is the formula ∀ x₁, …, xₙ ((Ψ₁(x₁,y₁,…,yₘ) ∧ … ∧ Ψₙ(xₙ,y₁,…,yₘ)) → φ(x,x₁,…,xₙ)).

Here, each formula Ψᵢ has m + 1 bound variables, one for expressing a predicate of an xᵢ, and m remaining ones. In the resulting formula, the bound variables are the m remaining bound variables plus x, while all of the original bound variables x₁,…,xₙ get bounded to a ∀ quantifier.

Intuitively, nestFormulaeFunc gives F(f₁(y₁,…,yₘ), …, fₙ(y₁,…,yₘ)), the result of substituting functions f₁, … fₙ into a function F, using the defining formulae of their graphs (xᵢ = fᵢ(y₁,…,yₘ) iff Ψᵢ(xᵢ,y₁,…,yₘ), and x = F(x₁,…,xₙ) iff φ(x,x₁,…,xₙ)).

Equations

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

theorem FFL.FirstOrder.Semiformula.eval_nestFormulae {L : Language} {ξ : Type u_1} {M : Type u_2} [s : Tarski.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 FFL.FirstOrder.Semiformula.eval_nestFormulae₀ {L : Language} {ξ : Type u_1} {M : Type u_2} [s : Tarski.Structure L M] {f : ξ → M} {n✝ : ℕ} {e : Fin n✝ → M} {φ : Semiformula L ξ 0} : (Eval e f) (φ.nestFormulae ![]) ↔ (Eval ![] f) φ

@[simp]

theorem FFL.FirstOrder.Semiformula.eval_nestFormulae₁ {L : Language} {ξ : Type u_1} {M : Type u_2} [s : Tarski.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 FFL.FirstOrder.Semiformula.eval_nestFormulae₂ {L : Language} {ξ : Type u_1} {M : Type u_2} [s : Tarski.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 FFL.FirstOrder.Semiformula.eval_nestFormulae₃ {L : Language} {ξ : Type u_1} {M : Type u_2} [s : Tarski.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 FFL.FirstOrder.Semiformula.eval_nestFormulae₄ {L : Language} {ξ : Type u_1} {M : Type u_2} [s : Tarski.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 FFL.FirstOrder.Semiformula.eval_nestFormulaeFunc {L : Language} {ξ : Type u_1} {M : Type u_2} [s : Tarski.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 FFL.FirstOrder.Semiformula.eval_nestFormulaeFunc₀ {L : Language} {ξ : Type u_1} {M : Type u_2} [s : Tarski.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 FFL.FirstOrder.Semiformula.eval_nestFormulaeFunc₁ {L : Language} {ξ : Type u_1} {M : Type u_2} [s : Tarski.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 FFL.FirstOrder.Semiformula.eval_nestFormulaeFunc₂ {L : Language} {ξ : Type u_1} {M : Type u_2} [s : Tarski.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 FFL.FirstOrder.Semiformula.eval_nestFormulaeFunc₃ {L : Language} {ξ : Type u_1} {M : Type u_2} [s : Tarski.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 FFL.FirstOrder.Semiformula.eval_nestFormulaeFunc₄ {L : Language} {ξ : Type u_1} {M : Type u_2} [s : Tarski.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 FFL.FirstOrder.BinderNotation.finSuccItr {n : ℕ} (i : Fin n) (m : ℕ) : Fin (n + m)

Equations

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

(Literal) Notation for terms

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

Equations

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

def Lean.Parser.Category.first_order_term : Category

Equations

• Lean.Parser.Category.first_order_term = { }

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

Equations

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

def FFL.FirstOrder.BinderNotation.first_order.quote_type.quot : Lean.ParserDescr

Equations

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

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

Equations

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

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

Equations

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

def FFL.FirstOrder.BinderNotation.«term⤫term(_)[_|_|_]» : Lean.ParserDescr

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

A term with free variables.

Equations

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

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

A term with bound variables.

Equations

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

def FFL.FirstOrder.BinderNotation.unexpanderNatLit : Lean.PrettyPrinter.Unexpander

Equations

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

def FFL.FirstOrder.BinderNotation.unexpanderOperatorConst : Lean.PrettyPrinter.Unexpander

Equations

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

def FFL.FirstOrder.BinderNotation.unexpanderAdd : Lean.PrettyPrinter.Unexpander

Equations

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

def FFL.FirstOrder.BinderNotation.unexpanderMul : Lean.PrettyPrinter.Unexpander

Equations

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

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

Equations

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

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

Equations

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

Notation for formulae

def FFL.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 FFL.FirstOrder.BinderNotation.«term⤫formula(_)[_|_|_]» : Lean.ParserDescr

Equations

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

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

Equations

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

def FFL.FirstOrder.BinderNotation.«first_order_formulaOf_term[_]» : Lean.ParserDescr

Equations

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

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

Equations

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

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

Equations

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

def FFL.FirstOrder.BinderNotation.«first_order_formula%__⋯» : Lean.ParserDescr

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def FFL.FirstOrder.BinderNotation.«first_order_formula∀¹_» : Lean.ParserDescr

Equations

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

def FFL.FirstOrder.BinderNotation.«first_order_formula∃¹_» : Lean.ParserDescr

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def FFL.FirstOrder.BinderNotation.unexpanderEq : Lean.PrettyPrinter.Unexpander

Equations

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

def FFL.FirstOrder.BinderNotation.unexpanderLe : Lean.PrettyPrinter.Unexpander

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def FFL.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 FFL.FirstOrder.BinderNotation.«termF‘_’» : Lean.ParserDescr

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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