Stream: Beginner Questions

Topic: TYPE and itself

Tobias Heindel (Heliax GmbH) (May 03 2024 at 12:52):

Is there an FAQ where I would find this?

• TYPE
• itself

cf. https://isabelle.zulipchat.com/#narrow/stream/247541-Mirror.3A-Isabelle-Users-Mailing-List/topic/.5Bisabelle.5D.20Mysteries.20of.20locales.2C.20.22TYPE.28T.29.22.2C.20and.20.22T.20itself.22/near/299926087

Mathias Fleury (May 03 2024 at 12:55):

There are only some efforts but no centralized FAQ

Mathias Fleury (May 03 2024 at 12:57):

research has become much worse since the mailing list is not indexed anymore

Tobias Heindel (Heliax GmbH) (May 03 2024 at 12:58):

Mathias Fleury said:

research has become much worse since the mailing list is not indexed anymore

we'll figure it out all in time ... no need to dispair

Mathias Fleury (May 03 2024 at 12:59):

sorry I meant search, not research

Kevin Kappelmann (May 03 2024 at 13:16):

Note that there is a mirror of the isabelle users mailing list on zulip: https://isabelle.zulipchat.com/#narrow/stream/336180-Archive-Mirror.3A-Isabelle-Users-Mailing-List/topic/stream.20events/near/294997473

You can use the Zulip search to query the messages.

Mathias Fleury (May 03 2024 at 13:17):

Correct, but my favorite search engine has never suggested an email from the mailing list from the zulip mirror

Mathias Fleury (May 03 2024 at 13:18):

And the messages only go back to 2020

Kevin Kappelmann (May 03 2024 at 13:21):

No - the archive includes all messages up to 2020-08 and the Mirror stream includes all messages starting from 2020-08:

https://isabelle.zulipchat.com/#narrow/stream/336180-Archive-Mirror.3A-Isabelle-Users-Mailing-List/topic/stream.20events/near/294997692

Kevin Kappelmann (May 03 2024 at 13:22):

Here's the archive
https://isabelle.zulipchat.com/#narrow/stream/336180-Archive-Mirror.3A-Isabelle-Users-Mailing-List

Here's the mirror for the users mailing list:
https://isabelle.zulipchat.com/#narrow/stream/247541-Mirror.3A-Isabelle-Users-Mailing-List

Here's the mirror for isabelle dev:
https://isabelle.zulipchat.com/#narrow/stream/247542-Mirror.3A-Isabelle-Development-Mailing-List

Kevin Kappelmann (May 03 2024 at 14:05):

Tobias Heindel (Heliax GmbH) said:

Is there an FAQ where I would find this?

• TYPE
• itself

cf. https://isabelle.zulipchat.com/#narrow/stream/247541-Mirror.3A-Isabelle-Users-Mailing-List/topic/.5Bisabelle.5D.20Mysteries.20of.20locales.2C.20.22TYPE.28T.29.22.2C.20and.20.22T.20itself.22/near/299926087

Maybe the implementation manual gives you some idea what it is:
https://isabelle.in.tum.de/doc/implementation.pdf#subsection.2.3.2

Tobias Heindel (Heliax GmbH) (May 03 2024 at 14:47):

Kevin Kappelmann said:

Tobias Heindel (Heliax GmbH) said:

Is there an FAQ where I would find this?

• TYPE
• itself

cf. https://isabelle.zulipchat.com/#narrow/stream/247541-Mirror.3A-Isabelle-Users-Mailing-List/topic/.5Bisabelle.5D.20Mysteries.20of.20locales.2C.20.22TYPE.28T.29.22.2C.20and.20.22T.20itself.22/near/299926087

Maybe the implementation manual gives you some idea what it is:
https://isabelle.in.tum.de/doc/implementation.pdf#subsection.2.3.2

It gives me some information, indeed:

The TYPE constructor is the canonical representative of the unspecified type α itself; it essentially injects the language of types into that of terms. There is specific notation TYPE(τ) for TYPE_{τ itself}. Although being devoid of any particular meaning, the term TYPE(τ) accounts for the type τ within the term language. In particular, TYPE(α) may be used as formal argument in primitive definitions, in order to circumvent hidden polymorphism (cf. §2.2). For example, c TYPE(α) ≡ A[α] defines c :: α itself ⇒ prop in terms of a proposition A that depends on an additional type argument, which is essentially a predicate on types.

However, I wonder whether I have chosen the wrong category ... (Beginner Questions) ... :thinking:

Last updated: Feb 01 2025 at 20:19 UTC