|Page 212 of 800||Search internet|
denotes a data structure which represents the term . We shall refer to the brackets around as Gödel brackets, and to as the quoted version of . We shall refer to the value of a quote as a parse tree.The quoting construct has many, unusual properties. Among others, it does not respect substitution of equals. As an example, the value of differs from the value of even though . If one asks Logiweb to compute the value of , the value will be .
Maybe even more surprising, if one asks Logiweb to compute , then that value will also be . That is so because does not just denote the term as such. Each instance of denotes that particular instance of . Each instance contains so-called debugging information which encodes the exact location of the instance on the page. Among others, that debugging information is used when generating meaningful error messages.
One may think of debugging information as a sort of 'radioactive mark' on a term. The mark does not really affect the properties of the term, but it allows to trace a term through processes like macro and tactic expansion.
|Page 212 of 800||Search logiweb.eu|