aboutsummaryrefslogtreecommitdiff
path: root/spartan
diff options
context:
space:
mode:
authorJosh Chen2020-04-02 19:31:33 +0200
committerJosh Chen2020-04-02 19:31:33 +0200
commit0ddab0fe11c33fc559fc8fb58528618efdbc93a4 (patch)
tree28a770adf15d3284e1d7b0c3791fcd42851b5180 /spartan
parent6e88bdadd13cc5c8502bbddf01bd609baca8fc67 (diff)
better lambda notation
Diffstat (limited to 'spartan')
-rw-r--r--spartan/theories/Spartan.thy11
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"