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


            
            450.lean:2:11-2:12: error: don't know how to synthesize placeholder

            
            context:

            
            ⊢ ?m

            
            450.lean:2:6-2:7: error: failed to infer 'let' declaration type
	450.lean:2:11-2:12: error: don't know how to synthesize placeholder
	context:
	⊢ ?m
	450.lean:2:6-2:7: error: failed to infer 'let' declaration type