Documentation

Foundation.Vorspiel.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 : αβ
Instances
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      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 : αβ
      Instances