Re: [isabelle] Limit cardinals



If you want to do cardinals properly, there’s always Isabelle/ZF…

Larry Paulson


On 26 Sep 2014, at 17:21, Eddy Westbrook <westbrook at kestrel.edu> wrote:

> Hi,
> 
> How does one build a limit cardinal in Isabelle from an ascending sequence of cardinals?
> 
> For example, if I start from the types nat, nat -> bool, (nat -> bool) -> bool, etc., is it possible to create a type into which I can embed all of these types?
> 
> Thanks,
> -Eddy





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.