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


            
            autoPPExplicit.lean:2:26-2:31: error: application type mismatch

            
              @Eq.trans α a (b = c)

            
            argument

            
              b = c

            
            has type

            
              Prop : Type

            
            but is expected to have type

            
              α : Sort u_1
	autoPPExplicit.lean:2:26-2:31: error: application type mismatch
	@Eq.trans α a (b = c)
	argument
	b = c
	has type
	Prop : Type
	but is expected to have type
	α : Sort u_1