Thu, 07 Nov 2013 16:08:19 +1100 | kleing | Add output translation for <a := .., b := .., ..> state notation. | changeset | files |
Thu, 07 Nov 2013 02:42:20 +0100 | blanchet | reintroduce mutually (co)rec check, since the underlying N2M code doesn't quite handle the general case (esp. in presence of type variables) | changeset | files |
Thu, 07 Nov 2013 01:01:04 +0100 | blanchet | more docs | changeset | files |
Thu, 07 Nov 2013 00:37:18 +0100 | blanchet | properly detect when to perform n2m -- e.g. handle the case of two independent functions on irrelevant types being defined in parallel | changeset | files |
Wed, 06 Nov 2013 23:05:44 +0100 | blanchet | reverted 3e1d230f1c00 -- pervasiveness is useful, cf. Coinductive_Nat in the AFP | changeset | files |
Wed, 06 Nov 2013 22:50:12 +0100 | blanchet | simplified code | changeset | files |
Wed, 06 Nov 2013 22:42:54 +0100 | blanchet | fourth attempt at generalizing N2M types (to leverage caching) | changeset | files |
Wed, 06 Nov 2013 21:40:41 +0100 | blanchet | tuning | changeset | files |