`norm_swap` #

Evaluating swap x y z for numerals x y z that are ℕ, ℤ, or ℚ, via a norm_num plugin. Terms are passed to eval, quickly failing if not of the form swap x y z. The expressions for numerals x y z are converted to nat, and then compared. Based on equality of these nats, equality proofs are generated using either equiv.swap_apply_left, equiv.swap_apply_right, or swap_apply_of_ne_of_ne.

source

meta def norm_swap.eval :

expr → tactic (expr × expr)

A norm_num plugin for normalizing equiv.swap a b c where a b c are numerals of ℕ, ℤ, ℚ or fin n.

example : equiv.swap 1 2 1 = 2 := by norm_num

norm_swap #

`norm_swap` #