Re: [isabelle] Limit cardinals
If you want to do cardinals properly, there’s always Isabelle/ZF…
On 26 Sep 2014, at 17:21, Eddy Westbrook <westbrook at kestrel.edu> wrote:
> 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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and