Email Gateway (Aug 18 2022 at 10:06): Email Gateway (Aug 18 2022 at 10:06):From: Martin Klebermaß <martin@klebermass.de>
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@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
============================
smime.p7s
Email Gateway (Aug 18 2022 at 10:06):From: Tobias Nipkow <nipkow@in.tum.de>
Martin Klebermaß wrote:
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
Last updated: May 03 2024 at 12:27 UTC