You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
@PatrickMassot Is this a problem? The example right before shows that this particular case is solved by rfl. But, more generally, simp [fac] will replace fac 0 by 1 in any context. It seems strange to modify the example just to make that point.
A bigger issue is that we now only have a minimal discussion of decide in 5.3, and we never say that simp calls decide. Shall we replace this issue by a separate issue that says that we should expand the discussion of decide?
In Chapter 5, we have
which is misleading since giving
[fac]
plays no role.The text was updated successfully, but these errors were encountered: