I think the -> tactic in [-> ->] in the 'example' in ssec:specs, and the
/eqP-> version in sec:infprimes are used for the first time; but appeared not to be adequately explained. There is discussion later about /leq_trans-> in the context of partial views, but even there, the exact way how \C{n} got fixed to \C{n1} was not clear to me.
'idP .. is seldom used .. with iffP': not sure if you meant 'often' used instead of 'seldom'?
In sec:infprimes, the exists2 notation and the ?lemma tactic syntax were used but not defined.
gares
commented
6 years ago
I think the -> tactic in [-> ->] in the 'example' in ssec:specs, and the /eqP-> version in sec:infprimes are used for the first time; but appeared not to be adequately explained. There is discussion later about /leq_trans-> in the context of partial views, but even there, the exact way how \C{n} got fixed to \C{n1} was not clear to me.
'idP .. is seldom used .. with iffP': not sure if you meant 'often' used instead of 'seldom'?
In sec:infprimes, the exists2 notation and the ?lemma tactic syntax were used but not defined.