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


            
            axiom n : Type → Type

            
            section

            
            local notation "ℕ" x => n x

            
            end

            
            #check n Nat -- should *not* be `ℕ Nat : Type`
	axiom n : Type → Type
	section
	local notation "ℕ" x => n x
	end
	#check n Nat -- should not be `ℕ Nat : Type`