Re: [Hol-info] Converting ordinals from different type variables?

Hi Michael, Thanks very much, this saves me lots of time trying to prove something impossible. Regards, Chun Tian On 16 October 2017 at 00:59, wrote: > The definition is fine, but will not have the nice properties you want > (e.g., monotonicity) if the

Re: [Hol-info] Converting ordinals from different type variables?

The definition is fine, but will not have the nice properties you want (e.g., monotonicity) if the domain type is bigger than the range. In particular if your domain includes \omega_1 and the range only has countable ordinals, then the result of c2a on \omega_1 will be unspecified. This is

[Hol-info] Converting ordinals from different type variables?

Hi, If I have the following recursive function on ordinals, simply converting ‘c ordinals into the “same” ‘a ordinals: (* Construct a 'c ordinal from 'a ordinal *) val c2a_def = new_specification ( "c2a_def", ["c2a"], ord_RECURSION |> INST_TYPE [``:'a`` |-> ``:'c``] |>