core / init.meta.match_tactic

meta structure tactic.pattern :

target : expr
uoutput : list level
moutput : list expr
nuvars : ℕ
nmvars : ℕ

A pattern is an expression target containing temporary metavariables. A pattern also contains a list of outputs which also depend on these temporary metavariables. When we run match p e, the system will match p.target with e and assign the temporary metavariables. It then returns the outputs with the assigned variables.

Fields #

target Term to match. Contains temporary metavariables.
uoutput List of universes that are returned on a successful match.
moutput List of expressions that are returned on a successful match.
nuvars Number of (temporary) universe metavariables in this pattern.
nmvars Number of (temporary) metavariables in this pattern.

Example #

The pattern for list.cons h t returning h and t would be

{ target  := `(@list.cons ?x_0 ?x_1 ?x_2),
  uoutput := [],
  moutput := [?x_1,?x_2],
  nuvars  := 0,
  nmvars  := 3
}

Instances for tactic.pattern

tactic.pattern.has_to_tactic_format

source

meta constant tactic.mk_pattern (umetas : list level) (emetas : list expr) (target : expr) (uoutput : list level) (eoutput : list expr) :

tactic tactic.pattern

mk_pattern umetas emetas target uoutput eoutput creates a new pattern. The arguments are

umetas a list of level params to be replaced with temporary universe metavariables.
emetas a list of local constants to be replaced with temporary metavariables.
target the expression to be matched.
uoutput a list of levels to return upon matching. Fails if this depends on metavariables.
eoutput a list of expressions to return upon matching. Fails if this depends on metavariables.

The procedure is as follows:

Convert all metavariables in target to temporary metavariables.
For each item in umetas amd emetas, create a temporary metavariable and replace each instance of the item in target with a temporary metavariable
Replace these instances in uoutput and eoutput too.
Return these replaced versions as a pattern.

Example #

Let h,t be exprs with types α and list α respectively. Then mk_pattern [] [α,h,t](@list.cons α h t) [] [h,t]wouldmatch_pattern` against any expr which is a list.cons constructor and return the head and tail arguments.

source

meta constant tactic.match_pattern (p : tactic.pattern) (e : expr) (m : tactic.transparency := tactic.transparency.reducible) :

tactic (list level × list expr)

mk_pattern p e m matches (pattern.target p) and e using transparency m. If the matching is successful, then return the instantiation of pattern.output p. The tactic fails if not all (temporary) meta-variables are assigned.

source

meta def tactic.pexpr_to_pattern (p : pexpr) :

tactic tactic.pattern

Given a pre-term of the form λ x₁ ... xₙ, t[x₁, ..., xₙ], converts it into the pattern t[?x₁, ..., ?xₙ] with outputs [?x₁, ..., ?xₙ]

source

meta def tactic.match_expr (p : pexpr) (e : expr) (m : tactic.transparency := tactic.transparency.reducible) :

tactic (list expr)

Convert pre-term into a pattern and try to match e. Given p of the form λ x₁ ... xₙ, t[x₁, ..., xₙ], a successful match will produce a list of length n.

source