[Agda] Some observations about μν

Peter Hancock hancock at spamcop.net
Sat Jul 11 08:49:15 CEST 2009

Previous message: [Agda] Some observations about μν
Next message: [Agda] Congruence and substitutivity rules in heterogeneous equality
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

mu X. nu Y. 1 + X * Y

ie. mu X. colist X

That seems to be quite a nice version of the second
number class.

Hank

Previous message: [Agda] Some observations about μν
Next message: [Agda] Congruence and substitutivity rules in heterogeneous equality
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

More information about the Agda mailing list