Stream: Beginner Questions

Topic: Using bound type variables in a type_synonym


view this post on Zulip Jakub Kądziołka (Jan 18 2021 at 11:52):

I have a context that fixes some type variables:

context
  fixes blue :: 'color
  assumes population: "card (UNIV::'people set) = 200"
begin

(if you're wondering, I'm experimenting with the xkcd blue eyes puzzle)

Inside of this context, I want to introduce another type:

type_synonym world = "'people ⇒ 'color"

Isabelle doesn't like this:

Ignoring sort constraints in type variables(s): "'people", "'color"
in type abbreviation "world"
Extra variables on rhs: "'color", "'people"
The error(s) above occurred in type abbreviation "world"

What can I do to avoid repeating 'people => 'color everywhere?

view this post on Zulip Manuel Eberl (Jan 18 2021 at 11:53):

If you're just experimenting, you could axiomatise the types color and people instead.

view this post on Zulip Manuel Eberl (Jan 18 2021 at 11:55):

I don't think there's any other way.

view this post on Zulip Manuel Eberl (Jan 18 2021 at 11:56):

if you want this abbreviation

view this post on Zulip Jakub Kądziołka (Jan 18 2021 at 11:59):

Argh. I guess I could do that, but I needed this before in a locale that I actually instantiated later

view this post on Zulip Manuel Eberl (Jan 18 2021 at 12:01):

Florian Haftmann is currently localising a lot of notation stuff.

view this post on Zulip Manuel Eberl (Jan 18 2021 at 12:01):

You can ask about this on the mailing list, maybe he has some perspective on this.


Last updated: Aug 13 2022 at 05:18 UTC