[opentheory-users] type definitions

[Ramana Kumar]

Is there a good reason for the defineTypeOp command to define new
constants as well as the new type operator?

It's causing me a bit of trouble when trying to write an article
writer for HOL4, because HOL4's type definition mechanism doesn't
introduce new constants as well. Those constants can be defined after
the type is defined (both by HOL4 and by other stack machine
commands), although that might require Hilbert choice to be present...
actually, if it does require select maybe that's a good reason to do
it your way, since the stack machine currently doesn't depend on any
constants existing (except =).

The HOL4 way of doing a type definition is given a theorem |- P t, to
assert |- ?rep. (∀x' x''. (rep x' = rep x'') ⇒ (x' = x'')) ∧ ∀x. P x ⇔
∃x'. x = rep x')... so it depends on exists and forall as well. I am
starting to see the reasons for the inconvenient defineTypeOp... were
they deliberate decisions to avoid those constants?

Anyway it seems like to write a HOL4 article writer, one would just
need to define some dummy constants every time some HOL4 code wants to
define a type operator without providing the names for abs and rep (in
order to be able to accurately log a defineTypeOp command); later if
they decide to define an abs and reps then there will just be two
pairs of constants around doing the same job.