Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] COERCION_GEN_ERROR ?


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

From: Peter Lammich <lammich@in.tum.de>
Hi

See the examples below.

Is it the expected behaviour of the coercion package to interfere with a
usual typing-error (Example1), and output a less informative
COERCION_GEN_ERROR instead (Example2)?

Admittedly, the example is a bit weird, as it uses Trueprop, but I would
have expected the coercion package not to suppress the error messages
from the type-checker.

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

From: Dmitriy Traytel <traytel@in.tum.de>
Hi Peter,

you are right: this low-level error is certainly nothing to be presented
to the user.

Interestingly, it does not occur in the standard setup due to the
declaration of the map function for the function type. I.e. the
following will give you a proper error message.

theory Scratch
imports Main
begin

declare [[coercion_enabled]]
declare [[coercion_map "%f g h x. g (h (f x))"]]
lemma "Trueprop A \<Longrightarrow> B";

I'll investigate further.

Dmitriy

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

From: Dmitriy Traytel <traytel@in.tum.de>
It is now fixed in the Isabelle repository (0f81eca1e473). Thanks for
reporting.

Dmitriy


Last updated: Mar 29 2024 at 08:18 UTC