[Agda] (long post) some semantics, some syntax

[Nils Anders Danielsson]

On 2008-11-11 22:24, Conor McBride wrote:
>
> The nice thing is that I've escaped from the tight
> spiral of dependency. I finished setting up the
> semantics before I went anywhere near the syntax!
> Then, somehow, the syntax works out just so, taking
> type as an index (it's a "prior notion") and value
> as a decoder (it comes afterwards).

Cool. An encoding of a dependently typed language without a single
substitution in sight.

> I wonder what happens next.

Can you normalise the terms, or will the higher-order indices bite you?

-- 
/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.