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> 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.