[Ur] where to put disjointness proof when concatenating two type level records?

Marc Weber marco-oweber at gmx.de
Thu Dec 15 15:06:20 EST 2011


I remembered correctly: The wiki talks about it:
http://www.impredicative.com/wiki/index.php/Disjointness_fun_-_creating_records_using_type_level_functions
quote "
    Constructing a record type taking two names and two types. Because
    disjointness can't be proofed at type level it must be done at
    expression level.
"

My goal was to write a type level projection function - but looks like I
can't do it for this reason.

Marc Weber



More information about the Ur mailing list