[isabelle] COERCION_GEN_ERROR ?



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.