mathlib documentation


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.

meta def norm_swap.eval  :

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