[Agda] Typed vs untyped lambda abstractions

[Paul van der Walt]

Hi Guillaume,

On Sat, Aug 25, 2012 at 18:19:41 +0200, quoth Guillaume Brunerie:
>    4. Using Agda's source code, is it easy to add type annotations to
>    lambdas? In other words, if I have a term in Agda's internal syntax (of
>    type Agda.Syntax.Internal.Term, I think), how do I translate it to a term
>    in a lambda calculus with typed lambdas?
>    I think I tried to find a suitable function in Agda's source code a few
>    weeks ago, but I did not find anything.

I don't know if I'm really answering your question, but for
something I'm doing I wanted typed lambda's as a result from the
`quoteTerm` keyword, i.e. I didn't want to lose information like
the x having type Nat here:

quoteTerm \ (x : Nat) -> x

Anyway, I have some modifications to the Agda source in my
personal fork [1], the interesting bits happen in
Agda.TypeChecking.Rules.Term and Agda.TypeChecking.Substitute.
Feel free to browse my changesets, hopefully they'll be relevant
to your question.

Cheers,
Paul

1. https://darcs.denknerd.org/darcsweb.cgi?r=Agda;a=summary
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 836 bytes
Desc: Digital signature
Url : http://lists.chalmers.se/pipermail/agda/attachments/20120825/fa25e155/attachment.bin