aboutsummaryrefslogtreecommitdiff
path: root/spartan
diff options
context:
space:
mode:
Diffstat (limited to 'spartan')
-rw-r--r--spartan/core/Spartan.thy2
-rw-r--r--spartan/core/implicits.ML6
2 files changed, 8 insertions, 0 deletions
diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy
index 411eedd..10caa30 100644
--- a/spartan/core/Spartan.thy
+++ b/spartan/core/Spartan.thy
@@ -362,6 +362,8 @@ translations
"_lam_i2 x b" \<rightharpoonup> "\<lambda>x. b"
"\<lambda>x. b" \<rightleftharpoons> "CONST lam_i (fn x. b)"
+translations "\<lambda>x. b" \<leftharpoondown> "\<lambda>x: A. b"
+
subsection \<open>Lambda coercion\<close>
\<comment> \<open>Coerce object lambdas to meta-lambdas\<close>
diff --git a/spartan/core/implicits.ML b/spartan/core/implicits.ML
index ab64b0f..2b63f49 100644
--- a/spartan/core/implicits.ML
+++ b/spartan/core/implicits.ML
@@ -1,3 +1,9 @@
+(* Title: implicits.ML
+ Author: Joshua Chen
+
+Implicit arguments.
+*)
+
structure Implicits :
sig