Hi Jasmin,
On 12/02/14 12:11, Jasmin Blanchette wrote:
Hi Andreas,
I saw that you used the discriminator =, but we already have functions
Option.is_none and List.null. So far, they have been mainly used for code generation, but
I have found them very convenient in in my codatatype usages
Hi Jasmin,
On 13/02/14 13:47, Jasmin Blanchette wrote:
Hi Andreas,
Am 13.02.2014 um 13:34 schrieb Andreas Lochbihler
andreas.lochbih...@inf.ethz.ch:
In summary, I do not want to replace _ = None and _ = [] with null and
is_none, I'd just like to make null and is_none somewhat official. I
Hi Andreas,
I read the comment to your changeset 3def821deb70, which says that Nat.pred
may show up in theorems generated by primcorec. This is fine, because the
destructor view for codatatypes goes well with discriminators and selectors
for datatypes. As I do not know where discriminators
