[Agda] Re: examples of tactics via reflection

[Dan Licata]

On Apr14, Nils Anders Danielsson wrote:
> On 2009-04-14 15:36, Dan Licata wrote:
> >When A is weakenable with B, the type Check(canWeaken A B) computes
> >definitionally to Unit, so there is no proof obligation.
> 
> It may be worth noticing that this works best when A and B are
> (sufficiently) closed terms. 

Believe me, I've noticed... :)

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.  I sometimes end up rolling this myself for a little fragment.
E.g. suppose you want to solve list containments like

(xs ++ ys) < zs  

given

xs < zs and ys < zs.

I don't see how to do this when ++ is a function and xs and ys are
variables, because you want to pattern-match and recognize ++.  But you
can recognize the appends in a quoted representation of the goal.

-Dan