On 10/24/2016 09:16 PM, Rob Arthan wrote: > I am pretty sure nothing has been published and, if you are right about (2.2), > then I don't think type definitions can be proof-theoretically conservative.
They could. You can try to argue by "unfolding" the type definitions. Again, the model-theoretic conservativity is stronger than the proof-theoretic in general. And here you don't have an existential quantifier for type constructors so you can use the approach as you did for constants. Ondrej ------------------------------------------------------------------------------ The Command Line: Reinvented for Modern Developers Did the resurgence of CLI tooling catch you by surprise? Reconnect with the command line and become more productive. Learn the new .NET and ASP.NET CLI. Get your free copy! http://sdm.link/telerik _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
