# Re: [isabelle] What are the atomic terms in Isabelle/HOL?

On 6/4/2012 10:54 AM, Ramana Kumar wrote:

No, there are type constants. They are also known as "type operators".
Every type is either a type variable or a type constant applied to a list
of argument types (the list may be empty).
...
Base types, type constructors, and function types are all kinds of type
constants, or can be viewed as such.
...
A function type could be thought of a type constant for functions with
arity 2 (taking the domain and range types as arguments).

`Yea, you're right. Not surprising. And TUM PhD theses are good for
``clarifying the Isabelle terminology.
`
Types tau are either type variables alpha or applications of type
constructors k^n with fixed arity n...
"Proving Theorems of Higher-Order Logic with SMT Solvers", page 4
http://www21.in.tum.de/~boehmes/phd_thesis.html

`So the atomic types are type variables and type constructors of arity 0.
``I guess.
`

`The HOL4 terminology in the HOL4 logic manual is not the perfect goto
``document for explaining the Isabelle termininology.
`

I'm not sure what "type constructors" refers to, but probably it's just a
synonym for type constants.

`It turns out that it's the opposite, that "type constants" is a synonym
``for "type constructors". Synonyms being what they are, that's not a
``problem.
`

If I'm getting some details of Isabelle wrong here,I'm sure the list will
point it out. I'm speaking primarily from my knowledge of HOL.

`The list doesn't appear to be overly concerned with enforcing correct
``word usage. Lists are busy sometimes.
`
--GB

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*