Zulip Chat Archive
Stream: general
Topic: nat.strong_rec_on'
Yury G. Kudryashov (Feb 23 2021 at 02:27):
What is the difference between docs#nat.strong_rec_on and docs#nat.strong_rec_on'?
Kevin Buzzard (Feb 23 2021 at 07:45):
One has a '?
Aah, the latter is tagged elab_as_eliminator?
Last updated: Dec 20 2023 at 11:08 UTC