[Agda] Re: examples of tactics via reflection

[Nils Anders Danielsson]

On 2009-04-15 02:38, Dan Licata wrote:
> 
> It would be nice for these sorts of things if Agda provided a quotation
> datatype representing the syntax of Agda programs, along with an unquote
> function.

Is unquote the construction which takes arbitrary program text and turns
it into its representation? In that case unquote must not be a function.
Consider the following example:

  bad : ∀ n → unquote (0 + n) ≡ unquote (n + 0)
  bad n = cong unquote (+-comm 0 n)

However, unquote could be a keyword which could only be used applied to
an argument.

We have discussed adding a reflection mechanism before. The main issue
is coming up with a nice representation. Should it be well-typed? How
should variables be handled?

-- 
/NAD



This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.