Notes

[mtzguido]

• 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:

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