Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] lift_bnf Subscript exception

view this post on Zulip Email Gateway (Aug 22 2022 at 12:29):

From: Manuel Eberl <eberlm@in.tum.de>
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

view this post on Zulip Email Gateway (Aug 22 2022 at 12:30):

From: Dmitriy Traytel <traytel@inf.ethz.ch>
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

view this post on Zulip Email Gateway (Aug 22 2022 at 12:30):

From: Dmitriy Traytel <traytel@inf.ethz.ch>
See isabelle/b8dc1fd7d900.

Dmitriy

Last updated: Nov 21 2024 at 12:39 UTC