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
Coding objects into semantic objects (e.g. individuals of a model of a theory)
- quote : α → β
Instances
Equations
- LO.«term✶_» = Lean.ParserDescr.node `LO.term✶_ 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "✶") (Lean.ParserDescr.cat `term 1024))