[isabelle] why does this definition work with wrong types



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" ("_;_ \<turnstile> _ : _" [80,80,80,80] 80)
translations
"CT;sEnv \<turnstile> e : C" \<rightleftharpoons> "(CT,sEnv,e,C) \<in> typing"
inductive typing
intros
t_dummy :
  "0;1 \<turnstile> 2 : 3"


Es grüßt Sie freundlich/best regards,
	Martin Klebermaß

============================
martin at klebermass.de
============================
Schweiz:
Tramstr. 107
CH-5034 Suhr

Deutschland:
Fuchsbergstr. 11
D-82223 Eichenau

Mobil(DE): +49 (0) 176 / 70073282
Telefon(DE): +49 (0) 8141 / 509040
Mobil(CH): +41 (0) 79 / 7870352
Telefon(CH): +41 (0) 32 / 5107586

============================

Attachment: smime.p7s
Description: S/MIME cryptographic signature



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