Re: [isabelle] COERCION_GEN_ERROR ?



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

Am 04.09.2012 19:24, schrieb Peter Lammich:
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.

--
   Peter

********* Example1 **********

theory Scratch
imports Main
begin

declare [[coercion_enabled]]
lemma "Trueprop A \<Longrightarrow> B";
*** exception COERCION_GEN_ERROR fn raised (line 636 of
"~~/src/Tools/subtyping.ML")
*** At command "lemma" (line 6 of "/home/lammich/Scratch.thy")

********* Example2 **********

declare [[coercion_enabled = false]]
lemma "Trueprop A \<Longrightarrow> B";
*** Type unification failed: Clash of types "prop" and "bool"
***
*** Type error in application: incompatible operand type
***
*** Operator:  Trueprop :: bool \<Rightarrow> prop
*** Operand:   A :: prop
***
*** At command "lemma" (line 6 of "/home/lammich/Scratch.thy")








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.