Stream: Isabelle/ML

Topic: Match subterms

Josh Chen (Oct 14 2019 at 10:34):

Is there already an implementation of a function that, given a term, returns subterms matching a given pattern?

I need to do custom "abbreviation expansion" and know about Pattern.rewrite_term, but I need to additionally process patterns appearing in my abbreviation.

Last updated: Dec 07 2023 at 16:21 UTC