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

[effectfully]

2015-04-24 19:51 GMT+04:00, Nils Anders Danielsson <nad at cse.gu.se>:
> 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.

Yes, but I'm not sure, if this is a problem or a task. I think it's OK
to turn off the termination checker, if you can prove on a paper, that
the code terminates. I cannot though.