In #Coq, ever wonder what goes in the brackets in `destruct x as [...]` or `intros [...]`? Wonder no more: https://coq.inria.fr/distrib/V8.8.2/refman/proof-engine/tactics.html#coq:tacn.intros
It has some neat features if you're into unreadable one-liner tactics (that noone is going to read anyway) like me.
Welcome to your niu world ! We are a cute and loving international community Ｏ(≧▽≦)Ｏ !
We are a moderated instance, that aren't supporting harassment nor hateful speech. But we aren't a "safe" space, we won't prevent you to interact with instances that aren't respecting our rules.
"Be conservative in what you send and liberal in what you receive." - Netiquette
The main language used here is English, but for most of us this isn't our main language, so it's a great place to learn!