NotationClass

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 : α → β

  Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

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 : α → β

  Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

Equations

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