[Hol-info] infix exception

[xiaoyu xu <zhu...@gm...>]

Hi everyone,
I met an exception when I "set_fixity "divides" (Infixr 450)"
I checked the exception.
It said
Exception raised at Parse.add_rule:
Grammer error: Attempt to have differently associated infixes (RIGHT and
NONASSOC) at same level(450)

I looked into the kananaskis-5-reference, I found that I couldn't define an
infix at this level, because this was where other notation was. I solved it,
use "set_fixity "divides" (Infixr 451)" or "set_fixity "divides"
(Infix(NONASSOC, 450))" instead.

My questions are:

1.what are the differences between (Infixr 450) and (Infix(NONASSOC, 450))?
Which file introduces this?
2.How can I know at which level I can define an infix, at which I can't?
3.Should I clear the definitions after my work, how can I clear that?

Thank you very much!