Email Gateway (Aug 19 2022 at 08:41): 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.
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
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: Nov 21 2024 at 12:39 UTC