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


            
            #check fun (α) [Repr α] => repr (α := α)

            
            #check fun (x y) => x

            
            -- conservatively interpret as pattern

            
            #check fun (x id) => x
	#check fun (α) [Repr α] => repr (α := α)
	#check fun (x y) => x
	-- conservatively interpret as pattern
	#check fun (x id) => x