adbrucker
/
isabelle-hacks
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Renamed ._ (_.) to .._ (_..) to avoid conflict with common match pattern.

This commit is contained in:
Achim D. Brucker 2018-06-25 18:59:05 +01:00
parent ec1db40bd9
commit 09aa5120f5
1 changed files with 4 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
Hiding_Type_Variables.thy
View File

@ -421,8 +421,8 @@ subsection\<open>Register Parse Translations\<close>
syntax "_tvars_wildcard" :: "type \<Rightarrow> type" ("'('_') _")
syntax "_tvars_wildcard_retval" :: "type \<Rightarrow> type \<Rightarrow> type" ("'('_, _') _")
syntax "_tvars_wildcard_sort" :: "sort \<Rightarrow> type \<Rightarrow> type" ("'('_::_') _")
syntax "_tvars_wildcard_right" :: "type \<Rightarrow> type" ("_ '_.")
syntax "_tvars_wildcard_left" :: "type \<Rightarrow> type" ("_ .'_")
syntax "_tvars_wildcard_right" :: "type \<Rightarrow> type" ("_ '_..")
syntax "_tvars_wildcard_left" :: "type \<Rightarrow> type" ("_ ..'_")
parse_ast_translation\<open>
[
@ -498,12 +498,12 @@ subsection\<open>Parse Translation\<close>
update_default_tvars_mode "_ foobar" (print_all,parse)
declare [[show_types]]
definition hide_tvar_A :: "'x \<Rightarrow> (('x::linorder) foobar) ._"
definition hide_tvar_A :: "'x \<Rightarrow> (('x::linorder) foobar) .._"
where "hide_tvar_A x = foo x"
assert[string_of_thm_equal,
thm_def="hide_tvar_A_def", str="hide_tvar_A (x::'x) = foo x"]
definition hide_tvar_A' :: "'x \<Rightarrow> (('x,'b) foobar) ._"
definition hide_tvar_A' :: "'x \<Rightarrow> (('x,'b) foobar) .._"
where "hide_tvar_A' x = foo x"
assert[string_of_thm_equal,
thm_def="hide_tvar_A'_def", str="hide_tvar_A' (x::'x) = foo x"]