[isabelle-dev] interpretation command: "show ?thesis" causes type error
brianh at cs.pdx.edu
Tue Oct 5 21:07:28 CEST 2010
When proving a lemma, the term abbreviation ?thesis typically has type
"bool", and saying "show ?thesis" usually works.
But with "interpretation", it doesn't work. Here is a toy example that
shows what I mean:
locale foo = fixes x :: "'a::type" assumes x: "x = x"
term "foo" (* it has type 'a => bool, as expected. *)
interpretation myfoo: foo True
term ?thesis (* "foo True" :: prop *)
*** Type unification failed: Clash of types "prop" and "bool"
*** Type error in application: incompatible operand type
*** Operator: Trueprop :: bool => prop
*** Operand: PROP ?thesis :: prop
*** At command "show"
I am using revision 1410c84013b9, but the same error occurs with the
last few release versions as well.
More information about the isabelle-dev