From 77df99b3ffa41395ced31785074525c85e35fee9 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Fri, 14 Aug 2020 19:55:38 +0200
Subject: minor

---
 spartan/core/Spartan.thy  | 2 ++
 spartan/core/implicits.ML | 6 ++++++
 2 files changed, 8 insertions(+)

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
 
-- 
cgit v1.2.3