Re: [TYPES] Admissibility of conversion rule for typed definitional equality
Meven Lennon-Bertrand <[email protected]> Tue, 16 Jun 2026 10:31:29 +0200
| Newsgroups | gmane.comp.science.types |
|---|---|
| Message-ID | <[email protected]> |
WyBUaGUgVHlwZXMgRm9ydW0sIGh0dHA6Ly9saXN0cy5zZWFzLnVwZW5uLmVkdS9tYWlsbWFuL2xp c3RpbmZvL3R5cGVzLWxpc3QgXQpIaSBXYXNzaW0sCgpJJ2QgYmUgdmVyeSBzdXJwcmlzZWQgaWYg dGhpcyBydWxlcyB3YXMgYWRtaXNzaWJsZSwgYWx0aG91Z2ggSSBkb24ndCAKcXVpdGUgaGF2ZSBh IGZvcm1hbCByZWZ1dGF0aW9uLgoKQnV0IGNvbnNpZGVyIHRoZSBmb2xsb3dpbmcgc2V0dGluZzog YSBmdW5jdGlvbiBmIDogKHggOiBuYXQpIC0+IFAgc3VjaCAKdGhhdCBQWzAveF0gPSBuYXQgLT4g bmF0LCBhbmQgYSB0ZXJtIHQgc3VjaCB0aGF0IHQgPSAwIDogbmF0LiBIb3cgZG8geW91IApkZWR1 Y2UgdGhhdCBmIDAgMCA9IGYgdCB0PyBGaXJzdCwgYnkgY29uZ3J1ZW5jZSBvZiBhcHBsaWNhdGlv biAoYW5kIApzaW5jZSBieSByZWZsZXhpdml0eSBmID0gZiA6ICh4IDogbmF0KSAtPiBQKSwgd2Ug aGF2ZSBmIDAgPSBmIHQgOiBQWzBdLiAKVG8gdXNlIGNvbmdydWVuY2UgYWdhaW4sIHRob3VnaCwg eW91IG5lZWQgdG8gdHVybiB0aGlzIGludG8gZiAwID0gZiB0IDogCm5hdCAtPiBuYXQuIEhvdyBh cmUgeW91IGdvaW5nIHRvIGRvIHRoYXQgd2l0aG91dCB0aGUgcnVsZSB5b3UgdGhpbmsgaXMgCmFk bWlzc2libGU/IFJlZmxleGl2aXR5LCBzeW1tZXRyeSBhbmQgdHJhbnNpdGl2aXR5IGRvbid0IGNo YW5nZSB0aGUgCnR5cGVzIGF0IHdoaWNoIHRoZSBjb252ZXJzaW9uKHMpIGhhcHBlbiwgc28gdGhl eSB3b24ndCBoZWxwLiBBbmQgYWxsIApvdGhlciBydWxlcyAoY29uZ3J1ZW5jZXMgYW5kIGJhc2lj IGVxdWFsaXRpZXMsIGxpa2UgzrIgYW5kIM63KSBjaGFuZ2UgdGhlIAp0ZXJtcy4gSSBndWVzcyB5 b3VyIGlkZWEgd2FzIHRvIHVzZSB0aGUgY29udmVyc2lvbiBydWxlIGZvciB0eXBhYmlsaXR5IApz aW5jZSB0aGF0IGFsbG93cyB5b3UgdG8gY29uY2x1ZGUgZiAwIDogbmF0IC0+IG5hdCwgYnV0IEkg ZG9uJ3QgdGhpbmsgCnRoYXQgdGhpcyBpcyBvZiBhbnkgdXNlIGhlcmUuCgpCZXN0LAoKTWV2ZW4g TEVOTk9OLUJFUlRSQU5EClBvc3Rkb2Mg4oCTIElucmlhICYgSVJJRiwgVW5pdmVyc2l0w6kgUGFy aXMgQ2l0w6kKaHR0cHM6Ly91cmxkZWZlbnNlLmNvbS92My9fX2h0dHA6Ly93d3cubWV2ZW4uYWNf XzshIUlCeldMVXMhUkxOSW9Tb1lxM05uT1NpUVpkQlJBZWltV0xEa2U1VHhtaHVKVkJVVlc2Y1ox bXhLSE5uUHpzY1pRN0pIUVFEaGtTYkh0QlBid25ZNUU1NUFTbVBKTmtISUtSdFJzdWR4MFFIdVZR JCAKCgpPbiAxNS8wNi8yMDI2IDE4OjAzLCBXYXNzaW0gQWl0IE1vdXNzYSB3cm90ZToKPiBbIFRo ZSBUeXBlcyBGb3J1bSwgaHR0cDovL2xpc3RzLnNlYXMudXBlbm4uZWR1L21haWxtYW4vbGlzdGlu Zm8vdHlwZXMtbGlzdCAgXQo+IEhleSBhbGwsCj4KPiBJbiB0aGUgdHlwZWQgcHJlc2VudGF0aW9u cyBvZiBkZWZpbml0aW9uYWwgZXF1YWxpdHkgZm9yIGRlcGVuZGVudGx5IHR5cGVkCj4gc3lzdGVt cyBJJ3ZlIGNvbWUgYWNyb3NzIChTdWNoIGFzIFVUVAo+IDxodHRwczovL3VybGRlZmVuc2UuY29t L3YzL19faHR0cHM6Ly93d3cubGZjcy5pbmYuZWQuYWMudWsvcmVwb3J0cy85NC9FQ1MtTEZDUy05 NC0zMDQvaW5kZXguaHRtbF9fOyEhSUJ6V0xVcyFVLTNHdVk0czFPSmxZaFM5dTE0TU82NHZGcVY1 TDNuam9fMW85dDNsdndqSG9QUWtXMW5YOHcyUU51SWs5Rl9leGFmU2NZY2FOcWd3WTZ6T2N2a2RT clhMT3FhR3puQ1FmRDAkID4gb3IgQWdkYQo+IExpdGUgPGh0dHBzOi8vdXJsZGVmZW5zZS5jb20v djMvX19odHRwczovL2plc3Blci5zaWthbmRhLmJlL2ZpbGVzL3RoZXNpcy1maW5hbC1kaWdpdGFs LnBkZl9fOyEhSUJ6V0xVcyFVLTNHdVk0czFPSmxZaFM5dTE0TU82NHZGcVY1TDNuam9fMW85dDNs dndqSG9QUWtXMW5YOHcyUU51SWs5Rl9leGFmU2NZY2FOcWd3WTZ6T2N2a2RTclhMT3FhR2hPS25z amskID4pLCB0aGVyZQo+IHNlZW1zIHRvIGJlIGEgY29udmVyc2lvbiBydWxlIG9mIHRoZSBmb3Jt IG9mICJJZiBhID0gYScgYXQgdHlwZSBBLCBhbmQgQSA9Cj4gQiB0aGVuIGEgPSBhJyBhdCB0eXBl IEIiLgo+Cj4gSSB3b3VsZCB0ZW5kIHRvIGJlbGlldmUgc3VjaCBhIHJ1bGUgaXMgYWRtaXNzaWJs ZS4gV291bGQgYW55b25lIGhhdmUgYQo+IHJlZnV0YXRpb24gb2YgdGhhdCwgb3Igc29tZSBleGFt cGxlIG9mIGEgd29yayBpbiB3aGljaCBzdWNoIGEgcnVsZSBpcyBub3QKPiBuZWVkZWQgPwo+Cj4g VGhhbmtzIQo+IFdhc3MKCg==