max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

cleanup(init/meta/tactic) removing obsolete meta constants

Browse source
This commit is contained in:
Scott Morrison 2018-02-11 08:46:12 +11:00 • committed by Leonardo de Moura
parent 1a9962011d
commit 5d094cf835
1 changed files with 1 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
library/init/meta/tactic.lean
View file

@ -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.