lean2/tests/lean/notation7.lean

import logic data.num
open num

constant f : num → num
constant g : num → num → num

notation A `:+1`:100000 := f A

check g 0:+1:+1 (1:+1 + 2:+1):+1

set_option pp.notation false

check g 0:+1:+1 (1:+1 + 2:+1):+1
refactor(library/data/num): break into pieces to reduce dependencies 2014-11-07 16:21:42 +00:00			`import logic data.num`
feat(frontends/lean): max precedence used by Lean is not max_uint anymore The motivation is to allow users to define notation with higher precedence than function application. 2014-11-07 15:51:40 +00:00			`open num`

			`constant f : num → num`
			`constant g : num → num → num`

			notation A `:+1`:100000 := f A

			`check g 0:+1:+1 (1:+1 + 2:+1):+1`

			`set_option pp.notation false`

			`check g 0:+1:+1 (1:+1 + 2:+1):+1`