Jakub Kądziołka (Jan 18 2021 at 11:52): 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?
Manuel Eberl (Jan 18 2021 at 11:53):If you're just experimenting, you could axiomatise the types color and people instead.
Manuel Eberl (Jan 18 2021 at 11:55):I don't think there's any other way.
Manuel Eberl (Jan 18 2021 at 11:56):if you want this abbreviation
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
Manuel Eberl (Jan 18 2021 at 12:01):Florian Haftmann is currently localising a lot of notation stuff.
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: Apr 19 2024 at 08:19 UTC