con con_type_level_record = fn (n :: Name) (n2 :: Name) (t :: Type) (t2 :: Type) => [n = t, n2 = t2]
main.ur|141 col 84| 141:100: Couldn't prove field name disjointness || Con 1: [n = ()] || Con 2: [n2 = ()] || Hnormed 1: [n = ()] || Hnormed 2: [n2 = ()] Can this be done ? Probably it should look like this: [[n] ~ [n2]] Marc Weber _______________________________________________ Ur mailing list [email protected] http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
