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


            
            etaStructIssue.lean:20:2-20:5: error: type mismatch

            
              rfl

            
            has type

            
              mkNat e x₁ = mkNat e x₁ : Prop

            
            but is expected to have type

            
              mkNat e x₁ = mkNat e.mk x₂ : Prop
	etaStructIssue.lean:20:2-20:5: error: type mismatch
	rfl
	has type
	mkNat e x₁ = mkNat e x₁ : Prop
	but is expected to have type
	mkNat e x₁ = mkNat e.mk x₂ : Prop