diff options
| author | Josh Chen | 2020-05-30 18:29:11 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-05-30 18:29:11 +0200 |
| commit | 68bbcdcca00ae85dcaeae3ba7858dff1aa4802a6 (patch) | |
| tree | 94678c24c0e6e7eeb41cb85f9053cd03c4d1b697 /spartan | |
| parent | 2e807b74bd0f4e9a2ccfcb861bef876dba5aa066 (diff) | |
inhabitation coercion should be syntax, not logical constant!
Diffstat (limited to 'spartan')
| -rw-r--r-- | spartan/core/Spartan.thy | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy index 004ba8d..9a6d884 100644 --- a/spartan/core/Spartan.thy +++ b/spartan/core/Spartan.thy @@ -294,8 +294,8 @@ val _ = Context.>> text \<open>Automatically insert inhabitation judgments where needed:\<close> -consts inhabited :: \<open>o \<Rightarrow> prop\<close> ("(_)") -translations "CONST inhabited A" \<rightharpoonup> "CONST has_type {} A" +syntax inhabited :: \<open>o \<Rightarrow> prop\<close> ("(_)") +translations "inhabited A" \<rightharpoonup> "CONST has_type {} A" section \<open>Lambda coercion\<close> |