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



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.