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


            
            def g {α : Type}   (a : α) := a

            
            def f {{α : Type}} (a : α) := a


            #check g

            
            #check f

            
            #check g 1

            
            #check f 1
	def g {α : Type} (a : α) := a
	def f {{α : Type}} (a : α) := a

	#check g
	#check f
	#check g 1
	#check f 1