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: Jul 15 2022 at 23:21 UTC