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


            
            isDefEqOffsetBug.lean:19:2-19:5: error: type mismatch

            
              rfl

            
            has type

            
              ?m = ?m : Prop

            
            but is expected to have type

            
              0 + 0 = 0 : Prop
	isDefEqOffsetBug.lean:19:2-19:5: error: type mismatch
	rfl
	has type
	?m = ?m : Prop
	but is expected to have type
	0 + 0 = 0 : Prop