Notes

- ~Lack of F*/Pulse inlining prevents having a single launch_kernel. Ideally we only need the MxN variant.~
- Typeclass for shareable resources
- Disambiguation via IDE: dropdown with options, click to fill in. Would it re-typecheck? Is that too bad?
- This should check:
```fstar
assume val foo : int -> slprop

ghost fn test
(x y : int)
requires foo x
ensures foo x
{
assert (foo _);
}
```
Plus, specifying an implicit with something like `foo _` should help in disambiguating.
- Hover for context
- Have Pulse automatically use extensionality wherever possible, e.g. by tagging the argument of an slprop with an extensionality principle.
- `under` syntax.
- ~Do softmax~