[Agda] Induction-induction in a tricky order

Nils Anders Danielsson nad at cse.gu.se
Wed Mar 16 16:33:31 CET 2016


On 2016-03-15 16:57, Jesper Cockx wrote:
> There also seems to be a difference between the old- and new-style
> mutual blocks when referencing datatypes.

ISTR that old-style mutual blocks are translated to new-style mutual
blocks internally.

-- 
/NAD


More information about the Agda mailing list