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(-)
(limited to 'spartan')
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