tests/lean/matchVarNames.lean.expected.out - third_party/github.com/leanprover/lean4 - Git at Google


            
            matchVarNames.lean:13:29-13:30: error: don't know how to synthesize placeholder

            
            context:

            
            α✝ : Type

            
            β : α✝ → Type u_1

            
            is : List α✝

            
            i i✝ : α✝

            
            is✝ : List α✝

            
            a : β i✝

            
            as : HList β is✝

            
            h : Member i is✝

            
            ⊢ Member i is✝
	matchVarNames.lean:13:29-13:30: error: don't know how to synthesize placeholder
	context:
	α✝ : Type
	β : α✝ → Type u_1
	is : List α✝
	i i✝ : α✝
	is✝ : List α✝
	a : β i✝
	as : HList β is✝
	h : Member i is✝
	⊢ Member i is✝