Re: [isabelle] Local Theory Parameterized by Types Only?



I don't think this will work for me. I'm generating the ACL grammar and
inference rules from a .ott file, and it seems that generating a
parameterized grammar is not supported by the ott tool. My planned
workaround was to wrap the ott output in a locale to fill in the missing
types.

Scott

On Mon, Nov 14, 2016 at 4:52 PM, Lars Hupel <hupel at in.tum.de> wrote:

> 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
>



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.