destruct b; auto.https://twitter.com/Jose_A_Alonso/status/1220237265726844928 …
-
-
neat! I learned two new tricks from that, thanks! (`intro []` and `case_eq`)
-
You might like some more vanilla intro-patterns then :) Not as powerful as the SSReflect patterns, but still can be combined in a not-so-trivial way, e.g. intros [=->%length_zero_iff_nil]. A couple examples and explanations are herehttps://github.com/tchajed/coq-tricks/blob/master/src/IntroPatterns.v …
Kraj razgovora
Novi razgovor -
Čini se da učitavanje traje već neko vrijeme.
Twitter je možda preopterećen ili ima kratkotrajnih poteškoća u radu. Pokušajte ponovno ili potražite dodatne informacije u odjeljku Status Twittera.