From 0ddab0fe11c33fc559fc8fb58528618efdbc93a4 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Thu, 2 Apr 2020 19:31:33 +0200
Subject: better lambda notation

---
 spartan/theories/Spartan.thy | 11 +++++++----
 1 file 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"
 
-- 
cgit v1.2.3