Generic term deconstruction decomposes a constructor application into its constructor and the list with children. This can be done using the # operator. The match strategy ?p1#(p2) decomposes a constructor application into its onstructor name and the list of direct subterms. Matching such a pattern against a term of the form C(t1,...,tn) results in a match of "C" against p1 and a match of [t1,...,tn] against p2.

For more information:

• Generic Traversal Strategies