PatternMatchPushDown(S, A, B)

patmatch1.spad line 311 [edit on github]

This packages provides tools for matching recursively in type towers.

fixPredicate : Mapping(Boolean, B) -> Mapping(Boolean, A)

fixPredicate(f) returns g defined by g(a) = f(a::B).

patternMatch : (A, Pattern(S), PatternMatchResult(S, B)) -> PatternMatchResult(S, B)

patternMatch(expr, pat, res) matches the pattern pat to the expression expr; res contains the variables of pat which are already matched and their matches. Note: this function handles type towers by changing the predicates and calling the matching function provided by A.