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?
If you're just experimenting, you could axiomatise the types
I don't think there's any other way.
if you want this abbreviation
Argh. I guess I could do that, but I needed this before in a locale that I actually instantiated later
Florian Haftmann is currently localising a lot of notation stuff.
You can ask about this on the mailing list, maybe he has some perspective on this.
Last updated: Sep 25 2022 at 23:25 UTC