Add dependency parameter to weighted sorries

[chrisflav]

Add an optional parameter to the wsorry term and tactic taking a list of names of constants to be added as dependencies in the dependency graph.
The motivation is having an analogue of the \uses{...} command of leanblueprint. It can be used to indicate dependencies of a declaration that are not yet used in the actual implementation.

Example syntax:

theorem foo : True := by
  wsorry 10 [Nat.add]

The implementation of wsorry is changed to add an entry to an environment extension. Querying used wsorrys is no longer done by traversing the expression.