Jeremy Avigad
Jeremy Avigad
How does the last option interact with caching? Can user extensions decide whether it is safe to use the cache?
Very good. Feel free to close this issue, or leave it open, whichever is more useful to you.
Now that the semester has begun at Carnegie Mellon, I am also pretty buried. I don't mind keeping the `injections` tactics on my to do list in the hopes that...
It is now mentioned briefly in _Logic_, and we start to use it more substantially in _Sets, Functions, and Relations_. We don't give a detailed discussion or exhaustive overview, but,...
I'd rather save this for a chapter on discrete mathematics. We should have examples of various kinds of proof by induction, and combinatorial reasoning with finite sets, finite sums, cardinality,...
Two options there: - Put the discrete math chapter first. - If the only uses are mild (like a straightforward definition by recursion or induction), just do them on the...
I think I addressed all these... I'll close next time I come back, if there are no objections.
It just guesses the pattern, right, and chooses its own names? I guess that is useful when the user doesn't have to look at the names, e.g, when automation will...
How does this work? Do we manually make up names, like "exercise_with_sequences"? Do users see the name? Is it displayed with the exercise?
Done!