diff options
| author | Josh Chen | 2020-04-02 19:31:33 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-04-02 19:31:33 +0200 |
| commit | 0ddab0fe11c33fc559fc8fb58528618efdbc93a4 (patch) | |
| tree | 28a770adf15d3284e1d7b0c3791fcd42851b5180 | |
| parent | 6e88bdadd13cc5c8502bbddf01bd609baca8fc67 (diff) | |
better lambda notation
| -rw-r--r-- | spartan/theories/Spartan.thy | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/spartan/theories/Spartan.thy b/spartan/theories/Spartan.thy index fb901d5..ac12937 100644 --- a/spartan/theories/Spartan.thy +++ b/spartan/theories/Spartan.thy @@ -63,11 +63,14 @@ axiomatization app :: \<open>o \<Rightarrow> o \<Rightarrow> o\<close> ("(1_ `_)" [120, 121] 120) syntax - "_Pi" :: \<open>idt \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close> ("(2\<Prod>_: _./ _)" 30) - "_lam" :: \<open>idt \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close> ("(2\<lambda>_: _./ _)" 30) + "_Pi" :: \<open>idt \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close> ("(2\<Prod>_: _./ _)" 30) + "_lam" :: \<open>pttrns \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close> ("(2\<lambda>_: _./ _)" 30) + "_lam2" :: \<open>pttrns \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close> translations - "\<Prod>x: A. B" \<rightleftharpoons> "CONST Pi A (\<lambda>x. B)" - "\<lambda>x: A. b" \<rightleftharpoons> "CONST lam A (\<lambda>x. b)" + "\<Prod>x: A. B" \<rightleftharpoons> "CONST Pi A (\<lambda>x. B)" + "\<lambda>x xs: A. b" \<rightharpoonup> "CONST lam A (\<lambda>x. _lam2 xs A b)" + "_lam2 x A b" \<rightharpoonup> "\<lambda>x: A. b" + "\<lambda>x: A. b" \<rightleftharpoons> "CONST lam A (\<lambda>x. b)" abbreviation Fn (infixr "\<rightarrow>" 40) where "A \<rightarrow> B \<equiv> \<Prod>_: A. B" |