*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] What are the atomic terms in Isabelle/HOL?*From*: Makarius <makarius at sketis.net>*Date*: Sun, 24 Jun 2012 21:09:37 +0200 (CEST)*Cc*: Ramana Kumar <rk436 at cam.ac.uk>, gottfried.barrow at gmx.com*In-reply-to*: <CAMej=24=CZSjwg5sUz9OnVTT31qagw5H6BBErsh3N7kPoOh3mg@mail.gmail.com>*References*: <4FCC2AE7.5020405@gmx.com> <4FCC4AF9.1060304@in.tum.de> <4FCCB56F.6040403@gmx.com> <CAMej=24=CZSjwg5sUz9OnVTT31qagw5H6BBErsh3N7kPoOh3mg@mail.gmail.com>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Mon, 4 Jun 2012, Ramana Kumar wrote:

Base types, type constructors, and function types are all kinds of type constants, or can be viewed as such. A base type might be ":bool", the type of propositions, which may be considered as the type constant "bool" applied to no arguments. (Indeed, every type constant has a fixed number, its arity, of arguments it ought to take.) A function type could be thought of a type constant for functions with arity 2 (taking the domain and range types as arguments). I'm not sure what "type constructors" refers to, but probably it's just a synonym for type constants. 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.

I know Isabelle also has type classes, which complicates the story a bit, but you haven't mentioned them so I won't say anything further.

By all this it now seems clear to me that atomic types are distinct from atomic terms.Indeed all types, atomic or not, are distinct from all terms, atomic or not, in higher-order logic (or "simple type theory").

Makarius

**References**:**[isabelle] What are the atomic terms in Isabelle/HOL?***From:*gottfried . barrow

**Re: [isabelle] What are the atomic terms in Isabelle/HOL?***From:*Tobias Nipkow

**Re: [isabelle] What are the atomic terms in Isabelle/HOL?***From:*gottfried . barrow

**Re: [isabelle] What are the atomic terms in Isabelle/HOL?***From:*Ramana Kumar

- Previous by Date: Re: [isabelle] making use of star
- Next by Date: [isabelle] Lazy Lists
- Previous by Thread: Re: [isabelle] What are the atomic terms in Isabelle/HOL?
- Next by Thread: [isabelle] Verification of C Programs
- Cl-isabelle-users June 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list