tests/lean/435.lean - third_party/github.com/leanprover/lean4 - Git at Google


            
            variable {α} (op : α → α → α)

            
            local infixr:60 " ∙ " => op

            
            example (x y : α) : x ∙ y = y ∙ x := sorry


            infixr:60 " *** " => op -- Error, only local notation can reference section variables
	variable {α} (op : α → α → α)
	local infixr:60 " ∙ " => op
	example (x y : α) : x ∙ y = y ∙ x := sorry

	infixr:60 " *** " => op -- Error, only local notation can reference section variables