Re: [isabelle] why does this definition work with wrong types
Martin Klebermaß wrote:
during review of my theorems i found a wrong definition of a set in my
For better reading i introduced a syntax for my defined sets.
In one case i introduced a wrong definition of the syntax i used a nat
list instead of a nat.
So why does this definition work, because i think it should not work (a
nat list is mapped to a nat)
theory syntaxdef imports Main
typing :: "(nat * nat * nat * nat) set"
"_typing" :: "[nat,nat,nat list,nat] \<Rightarrow> bool" ("_;_
Because this is just syntax, Isabelle (more or less, for parsing
reasons) ignores the precise types you give to "_typing". Thus things
may parse, but then the type checker would complain if you did actually
supply a list.
This archive was generated by a fusion of
Pipermail (Mailman edition) and