Re: [isabelle] How to access a locale type parameter in a quotient type definition
Possibly now is a good time to plug my own paper "Defining functions on equivalence classes”, which is available* from my webpage (https://www.cl.cam.ac.uk/~lp15/papers/refereed.html). In this I outline how one can create quotient constructions quite easily using the set-theoretic primitives of Isabelle/HOL. Obviously quotient_type is easier to use, but as discussed, it wants to introduce a type and there is no reason on earth to conflate quotient constructions with types.
* It is available via an ACM system that supposedly provides open access from the author’s own webpage. If it doesn’t work for you, please email me for a copy.
> On 8 Jul 2019, at 15:52, Wolfgang Jeltsch <wolfgang-it at jeltsch.info> wrote:
> Consider the following attempt of a locale definition:
> locale example =
> fixes R :: "['a, 'a] ⇒ bool"
> assumes is_equivalence: "equivp R"
> quotient_type Q = 'a / R
> Isabelle doesn’t accept the use of the type variable `'a` in the
> quotient type definition, although it does accept referring to `'a` in
> types. How can I define a quotient type for the type `'a`?
This archive was generated by a fusion of
Pipermail (Mailman edition) and