class LO.GoedelQuote (α : Sort u_1) (β : Sort u_2) : Sort (max (max 1 u_1) u_2)

Coding objects into syntactic objects (e.g. natural numbers, first-order terms)

• quote : α → β

Instances

• LO.Arith.instGoedelQuoteForallFin_arithmetization
• LO.Arith.instGoedelQuoteFunc_arithmetization
• LO.Arith.instGoedelQuoteRel_arithmetization
• LO.Arith.instGoedelQuote_arithmetization
• LO.FirstOrder.Derivation2.instGoedelQuoteFinsetSyntacticFormula_incompleteness
• LO.FirstOrder.Derivation2.instGoedelQuote_incompleteness
• LO.FirstOrder.Semiformula.goedelQuoteSyntacticFormulaToCodedFormula
• LO.FirstOrder.Semiformula.goedelQuoteSyntacticSemiformulaToCodedSemiformula
• LO.FirstOrder.Semiformula.instGoedelQuoteSentenceFormulaCodeIn
• LO.FirstOrder.Semiterm.Operator.GoedelNumber.instGoedelQuote
• LO.FirstOrder.Semiterm.instGoedelQuoteForallFinSyntacticSemitermSemitermVecCodeInCast
• LO.FirstOrder.Semiterm.instGoedelQuoteSyntacticSemitermSemitermCodeInCast

def LO.«term⌜_⌝» : Lean.ParserDescr

Equations

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

class LO.StarQuote (α : Sort u_1) (β : Sort u_2) : Sort (max (max 1 u_1) u_2)

Coding objects into semantic objects (e.g. individuals of a model of a theory)

• quote : α → β

def LO.«term✶_» : Lean.ParserDescr

Equations

• LO.«term✶_» = Lean.ParserDescr.node `LO.term✶_ 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "✶") (Lean.ParserDescr.cat `term 1024))