Re: [isabelle] lift_bnf Subscript exception



Hi Manuel,

indeed the type analysis for the types of the non emptiness witnesses in lift_bnf is a bit simple minded.

Iâll improve on this tomorrow.

Thanks for testing,
Dmitriy

> On 11 Jan 2016, at 17:35, Manuel Eberl <eberlm at in.tum.de> wrote:
> 
> The following fails in 3201ddb00097 (and most likely also Isabelle2016-RC0) with a Subscript exception:
> 
> typedef ('k, 'v) fmap = "{M :: ('k â 'v). finite (dom M)}"
>  by (rule exI[of _ Map.empty]) simp_all
> 
> lift_bnf (dead 'k, 'v) fmap [wits: "Map.empty :: 'k â 'v option"]
> (* exception Subscript raised (line 97 of "./basis/List.sml") *)
> 
> 
> Can anybody tell me why? Am I doing something wrong?
> 
> 
> Cheers,
> 
> Manuel
> 





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