blanchet [Thu, 07 Nov 2013 00:37:18 +0100] rev 54286
properly detect when to perform n2m -- e.g. handle the case of two independent functions on irrelevant types being defined in parallel
blanchet [Wed, 06 Nov 2013 23:05:44 +0100] rev 54285
reverted 3e1d230f1c00 -- pervasiveness is useful, cf. Coinductive_Nat in the AFP
blanchet [Wed, 06 Nov 2013 22:50:12 +0100] rev 54284
simplified code
blanchet [Wed, 06 Nov 2013 22:42:54 +0100] rev 54283
fourth attempt at generalizing N2M types (to leverage caching)
blanchet [Wed, 06 Nov 2013 21:40:41 +0100] rev 54282
tuning
hoelzl [Tue, 05 Nov 2013 21:23:42 +0100] rev 54281
int and nat are conditionally_complete_lattices
blanchet [Wed, 06 Nov 2013 14:50:50 +0100] rev 54280
be more open-minded and allow needless mutual recursion for 'prim(co)rec', since we allow it for '(co)datatype' -- eventual warnings (or errors) should be centralized in 'fp_bnf'
blanchet [Wed, 06 Nov 2013 13:00:45 +0100] rev 54279
removed dead code
blanchet [Wed, 06 Nov 2013 13:00:16 +0100] rev 54278
update docs
blanchet [Wed, 06 Nov 2013 12:47:50 +0100] rev 54277
take out possibility of moving corecursive calls past constructors -- this doesn't work in the general case