[isabelle] Problem with "additional type variables" in a definition
I'm having a problem with Isabelle 2016 which I've minimised to the following file. There seems to be something particular in how Isabelle handles types appearing in a definition but not in any arguments to the thing being defined.
definition foo :: "bool" ("f" 50) where
"foo â âx :: 'a. True"
abbreviation bar :: "bool" where
"bar â foo"
The definition gives the output
foo :: "bool"
Additional type variable(s) in specification of "foo": 'a
Dropping mixfix syntax ("foo"  50)
The abbreviation and lemma both give the output
Type unification failed: Clash of types "_ â _" and "bool"
Type error in application: incompatible operand type
Operator: op â bar :: bool â prop
Operand: foo :: ??'a itself â bool
Why is the mixfix syntax dropped?
Why has foo -- which was defined to be a constant and this was confirmed by the output -- become a function?
Is there a way to get the mixfix syntax and abbreviation to work?
Lars-Henrik Eriksson, PhD, Senior Lecturer
Computing Science, Dept. of Information Technology, Uppsala University, Sweden
This archive was generated by a fusion of
Pipermail (Mailman edition) and