--- a/src/CTT/CTT.thy Sun Aug 25 15:02:19 2024 +0200
+++ b/src/CTT/CTT.thy Sun Aug 25 15:07:22 2024 +0200
@@ -58,12 +58,12 @@
syntax
"_PROD" :: "[idt,t,t]\<Rightarrow>t" ("(3\<Prod>_:_./ _)" 10)
"_SUM" :: "[idt,t,t]\<Rightarrow>t" ("(3\<Sum>_:_./ _)" 10)
+syntax_consts
+ "_PROD" \<rightleftharpoons> Prod and
+ "_SUM" \<rightleftharpoons> Sum
translations
"\<Prod>x:A. B" \<rightleftharpoons> "CONST Prod(A, \<lambda>x. B)"
"\<Sum>x:A. B" \<rightleftharpoons> "CONST Sum(A, \<lambda>x. B)"
-syntax_consts
- "_PROD" \<rightleftharpoons> Prod and
- "_SUM" \<rightleftharpoons> Sum
abbreviation Arrow :: "[t,t]\<Rightarrow>t" (infixr "\<longrightarrow>" 30)
where "A \<longrightarrow> B \<equiv> \<Prod>_:A. B"