Re: [isabelle] lift_bnf Subscript exception



See isabelle/b8dc1fd7d900.

Dmitriy

> On 11 Jan 2016, at 21:52, Dmitriy Traytel <traytel at inf.ethz.ch> wrote:
> 
> 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.