[Agda] Type-preserving renaming and substitutions for a dependently typed lambda calculus.

[Nils Anders Danielsson]

On 2015-04-24 17:32, effectfully wrote:
> I wrote some code in order to understand what are the problems with
> the natural representation (a bunch of mutually defined datatypes with
> the usual semantics) equipped with implicit weakening and
> substitutions.

I guess you have already encountered a problem, because you have turned
off the termination checker.

-- 
/NAD