From 5d094cf8354d5ffccf87b20f208cc058f9aed175 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Sun, 11 Feb 2018 08:46:12 +1100 Subject: [PATCH] cleanup(init/meta/tactic) removing obsolete meta constants --- library/init/meta/tactic.lean | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index 08db2d815e..802c8253bc 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -415,13 +415,7 @@ meta constant get_assignment : expr → tactic expr Fail if argument is not a meta-variable. -/ meta constant is_assigned : expr → tactic bool meta constant mk_fresh_name : tactic name -/-- Return a hash code for expr that ignores inst_implicit arguments, - and proofs. -/ -meta constant abstract_hash : expr → tactic nat -/-- Return the "weight" of the given expr while ignoring inst_implicit arguments, - and proofs. -/ -meta constant abstract_weight : expr → tactic nat -meta constant abstract_eq : expr → expr → tactic bool + /-- Induction on `h` using recursor `rec`, names for the new hypotheses are retrieved from `ns`. If `ns` does not have sufficient names, then use the internal binder names in the recursor.