search

SKolodynski / IsarMathLib

IsarMathLib is a library of formalized mathematics for Isabelle/ZF.
https://isarmathlib.org
Other
16 stars 2 forks source link

Roelcke uniformity #14

Closed dan323 closed 4 years ago

dan323 commented 4 years ago
  1. Left and right translations uniformly continuous in their respective uniformities.
  2. Roelcke uniformity

Partially solves #4

SKolodynski commented 4 years ago

I got *** Failed to refine any pending goal *** At command "by" (line 494 of "~/Projects/IsarMathLib/IsarMathLib_git/IsarMathLib/TopologicalGroup_Uniformity_ZF.thy") after merge. I have fixed that but some element of the pull request process is still missing.

dan323 commented 4 years ago

What is missing?

SKolodynski commented 4 years ago

I imagine you have some workflow (process) for generating a pull request. It would be good if the result of applying the changes provided in the pull request always resulted in sources that can be verified with Isabelle. This is currently not the case as this error (easy to fix) shows. Something is missing in the process on your side.

dan323 commented 4 years ago

In this case I had to add a second commit to update to your master. This commit was done on github side. My original commit was working.

dan323 commented 4 years ago

Next time, in case of a second commit, I will do it on my side.