mathlib3 documentation

core / init.meta.comp_value_tactics

meta constant mk_nat_val_ne_proof :

expr → expr → option expr

meta constant mk_nat_val_lt_proof :

expr → expr → option expr

meta constant mk_nat_val_le_proof :

expr → expr → option expr

meta constant mk_fin_val_ne_proof :

expr → expr → option expr

meta constant mk_char_val_ne_proof :

expr → expr → option expr

meta constant mk_string_val_ne_proof :

expr → expr → option expr

meta constant mk_int_val_ne_proof :

expr → expr → option expr

meta def tactic.comp_val :

meta def tactic.interactive.comp_val :

Close goals of the form n ≠ m when n and m have type nat, char, string, int or subtypes {i : ℕ // p i}, and they are literals. It also closes goals of the form n < m, n > m, n ≤ m and n ≥ m for nat. If the goal is of the form n = m, then it tries to close it using reflexivity.