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 definition.

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 MHonArc.