diff options
| author | Josh Chen | 2020-05-28 16:00:31 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-05-28 16:00:31 +0200 |
| commit | 17b9392e7f5d568f6bfb5b0d552866e18c118762 (patch) | |
| tree | 6d30711a235a2b1dad99235789aea914179cc1c0 | |
| parent | 1ccd93665a01acdc25b37409e94b71615ced5393 (diff) | |
notation
| -rw-r--r-- | spartan/core/Spartan.thy | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy index b0fec5a..3d59464 100644 --- a/spartan/core/Spartan.thy +++ b/spartan/core/Spartan.thy @@ -115,6 +115,9 @@ translations "\<Sum>x: A. B" \<rightleftharpoons> "CONST Sig A (\<lambda>x. B)" abbreviation Prod (infixl "\<times>" 60) where "A \<times> B \<equiv> \<Sum>_: A. B" +abbreviation "and" (infixl "\<and>" 60) + where "A \<and> B \<equiv> A \<times> B" + axiomatization where SigF: "\<lbrakk>\<And>x. x: A \<Longrightarrow> B x: U i; A: U i\<rbrakk> \<Longrightarrow> \<Sum>x: A. B x: U i" and |