Page MenuHomeIsabelle/Phabricator

Fully localized type abbreviations
Open, WishlistPublic


Type abbreviations are permitted within a local theory target, but cannot refer to locally fixed type variables. So type_synonym is only half-localized (like typedecl and typedef).

This should be reconsidered eventually, but it will require to revisit many fine points in local theory targets, potentially also specification packages for types.

Example (e.g. Isabelle2019):

theory Scratch
  imports Main

locale test = fixes x :: 'a

type_synonym t = "'a × 'a" 
  Extra variables on rhs: "'a"
  The error(s) above occurred in type abbreviation "t"



Event Timeline

makarius triaged this task as Wishlist priority.Feb 19 2020, 8:43 PM
makarius created this task.