*To*: scott constable <sdconsta at syr.edu>, Peter Lammich <lammich at in.tum.de>*Subject*: Re: [isabelle] Local Theory Parameterized by Types Only?*From*: Lars Hupel <hupel at in.tum.de>*Date*: Mon, 14 Nov 2016 22:52:53 +0100*Cc*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <CADYF24cnQiTk3Af=TPZ0LH2-Qe=Th-GtE4cvvoLtrLN+MUjEiA@mail.gmail.com>*References*: <CADYF24fpmk3HkCE-70abs43KPjzPrKCzBHKZnfYvzs+A8SMw3A@mail.gmail.com> <201611142048.uAEKm0gE022275@mx2.syr.edu> <CADYF24cnQiTk3Af=TPZ0LH2-Qe=Th-GtE4cvvoLtrLN+MUjEiA@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.4.0

Dear Scott, > locale ACL = > fixes principal :: "'a itself" and command :: "'b itself" > begin > > datatype "princ" = -- {* Principal Expressions *} > p_PrincName "'a" -- {* Principal Name *} > | p_ConjWith "princ" "princ" -- {* Conjunction With *} > | p_Quoting "princ" "princ" -- {* Quoting *} > > but now Isabelle reports an error: "Extra type variables on right-hand side > "'a"". this is not possible in Isabelle/HOL. Instead, you can define the "princ" datatype, parameterized on 'a (and maybe 'b) outside of the locale. You can then use "('a, 'b) princ" inside the locale. Cheers Lars

**Follow-Ups**:**Re: [isabelle] Local Theory Parameterized by Types Only?***From:*scott constable

**References**:**[isabelle] Local Theory Parameterized by Types Only?***From:*scott constable

**Re: [isabelle] Local Theory Parameterized by Types Only?***From:*scott constable

- Previous by Date: Re: [isabelle] Local Theory Parameterized by Types Only?
- Next by Date: Re: [isabelle] Local Theory Parameterized by Types Only?
- Previous by Thread: Re: [isabelle] Local Theory Parameterized by Types Only?
- Next by Thread: Re: [isabelle] Local Theory Parameterized by Types Only?
- Cl-isabelle-users November 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list