More actions on kinds

[brprice]

Description

This is a feature request. We should have some more actions on kinds, for parity with terms and types.

Dependencies

None

Spec

We currently (as of #1120) have construction and deletion actions for kinds, and can use SetCursor and move to navigate. This lets us create any kind from any starting point, but is not as ergonomic/fully fleshed as actions for types and terms. In particular we do not have

• RaiseKind, so changing (* -> * -> *) -> (* -> *) into its LHS * -> * -> * is long-winded
• enter/exit kind movements, so scripting a "higher-level action" which, for example, creates a forall and sets its kind ∀f:*->*. ? is awkward-to-impossible: the only way to focus on the kind is by ID.

Implementation details

I believe this should be straightforward. We have not done this before as kinds were not exposed much in our frontend.

Not in spec

Discussion

This was initially thought about during development of #1120 (comment). @georgefst pointed out the somewhat related issues #1141 (comment) and #66 (comment).

Future work