Re: [isabelle] short-cut for defining inductive relations



On Tue, 28 Mar 2006, Holger Gast wrote:

> Constant declaration, syntax declaration, translation, and finally,
> the inductive definition.

> Is there any fundamental reason why a short-cut like
> 
> --- snip ---
> inductive_relations
>    wt_exp :: tyctx exp ty ("_ |-exp _ : _" [60,60] 60)
> intros
>  ...
> monos
>  ...
> --- snip ---
> 
> cannot replace the above four declarations by suitable
> calls to the Isabelle interface functions?

This is not as easy as it looks on the surface.  Nevertheless there are 
plans the re-implement the concept of inductive predicates in a more 
advanced manner (within a locale context etc.); this will also do away 
with the syntax/translations incantations.


	Makarius





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