[isabelle] Limit cardinals


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