diff options
| author | Josh Chen | 2020-08-14 19:55:38 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-08-14 19:55:38 +0200 |
| commit | 77df99b3ffa41395ced31785074525c85e35fee9 (patch) | |
| tree | 0b9f18ae2be9341bd69961023172cd95a3e65b19 | |
| parent | d172f9d35a9a1680ec15e4c61e5becbbc92d2ce7 (diff) | |
minor
| -rw-r--r-- | spartan/core/Spartan.thy | 2 | ||||
| -rw-r--r-- | spartan/core/implicits.ML | 6 |
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 |