Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] exception Option


view this post on Zulip Email Gateway (Aug 19 2022 at 08:43):

From: Henri.Debrat@loria.fr
Hi,

Does anyone know what I should do when encountering the following error:
exception Option raised (line 81 of "General/basics.ML")

I was using proof (auto dest: ext[OF _ _]) in case it might help.

Henri.

view this post on Zulip Email Gateway (Aug 19 2022 at 08:43):

From: Lars Noschinski <noschinl@in.tum.de>
Hi,

On 05.09.2012 14:16, Henri.Debrat@loria.fr wrote:

Does anyone know what I should do when encountering the following error:
exception Option raised (line 81 of "General/basics.ML")

This is an internal error and as such shouldn't reach the user. Without
knowing the exact situation, it is hard to see, where this issue stems from.

I was using proof (auto dest: ext[OF _ _]) in case it might help.

Can you give an complete minimal example (i.e. a complete theory file)?
Also, which version of Isabelle are you using?

-- Lars


Last updated: Nov 21 2024 at 12:39 UTC