I fully agree with Norm's demand that all theorems in set.mm (at least in
the main body of set.mm!) should be minimized, but I am of the same opinion
as @savask that tagging minimized/not minimized theorems as proposed by
Norm is not practicable and would make set.mm more clumsy.
At least I
I agree that minimization markers "add no value", so in my opinion they
should be kept out of set.mm altogether. Maybe we can create a file
"minimized_theorems" (something like "discouraged") which will be a list
of, well, minimized theorems :-) Contributors won't have to set any tags or
In the past, every year or two we would run "minimize_with" on the entire
set.mm. But as set.mm has grown, doing this has become a somewhat large
project. The last time was in Feb., which involved people volunteering
their CPUs over several weeks as well as my time managing it.
Benoît
> Yeah, I was somewhat involved in the research behind that paper. I think
> it's trying too hard to fit imperative style into a proofy language; it's
> difficult to be direct with that approach and there are certain kinds of
> constructions that are impossible with it (like getting the value
