case are referred to as "defective tactics": https://coq.inria.fr/distrib/current/refman/proof-engine/ssreflect-proof-language.html#the-defective-tactics
I'm curious what's "defective" about them.
Here, "defective" = lack "arguments".
So when the manual describes the defective move, it adds:
Of course this tactic is most often used in combination with the bookkeeping tacticals
I won’t claim that “defective” can mean “missing something” in English — but maybe in Latin/French?
back to ssreflect, I can’t remember/find where I read that “defective” is used in this sense (maybe in the ssreflect tutorial?), so a clarification in the manual would IMHO be welcome.
Last updated: Feb 08 2023 at 04:04 UTC