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


            
            1433.lean:11:49-11:52: error: type mismatch

            
              rfl

            
            has type

            
              ?m = ?m : Prop

            
            but is expected to have type

            
              dividend % divisor = wrongRem : Prop
	1433.lean:11:49-11:52: error: type mismatch
	rfl
	has type
	?m = ?m : Prop
	but is expected to have type
	dividend % divisor = wrongRem : Prop