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

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.


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