VER-520: Change (>>) for (>>_)

This is a know issue that was naively solved using `infixl ">>_"`
which effectively does nothing since "_" has an special meaning.
`infixl ">>'_"` was introduced to fix the issue. has a special meaning

  tags: [VER-520]
This commit is contained in:
Alejandro Gomez-Londono 2016-09-05 16:56:13 +10:00
parent 28c0c2ed1e
commit 6ed990f1da
1 changed files with 1 additions and 1 deletions

View File

@ -23,7 +23,7 @@ begin
abbreviation (input) "flip \<equiv> swp"
abbreviation(input) bind_drop :: "('a, 'c) nondet_monad \<Rightarrow> ('a, 'b) nondet_monad
\<Rightarrow> ('a, 'b) nondet_monad" (infixl ">>_" 60)
\<Rightarrow> ('a, 'b) nondet_monad" (infixl ">>'_" 60)
where "bind_drop \<equiv> (\<lambda>x y. bind x (K_bind y))"
lemma bind_drop_test: