aboutsummaryrefslogtreecommitdiff
path: root/spartan
diff options
context:
space:
mode:
authorJosh Chen2020-05-30 18:29:11 +0200
committerJosh Chen2020-05-30 18:29:11 +0200
commit68bbcdcca00ae85dcaeae3ba7858dff1aa4802a6 (patch)
tree94678c24c0e6e7eeb41cb85f9053cd03c4d1b697 /spartan
parent2e807b74bd0f4e9a2ccfcb861bef876dba5aa066 (diff)
inhabitation coercion should be syntax, not logical constant!
Diffstat (limited to 'spartan')
-rw-r--r--spartan/core/Spartan.thy4
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>