Re: [isabelle] why does this definition work with wrong types



Martin Klebermaß wrote:
Hello,

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

begin

consts
  typing  :: "(nat * nat * nat * nat) set"
syntax
"_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.

Tobias





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.