| ~SPC m ,~ | Shows the type of the goal at point and the currect context. |
| ~SPC m .~ | Shows the context, the goal and the given expression's inferred type. |
| ~SPC m a~ | Simple proof search. |
| ~SPC m b~ | Go to the previous goal, if any and activate goal-navigation micro-state. |
| ~SPC m c~ | Refine the pattern variables given in the goal. |
| ~SPC m d~ | Infers the type of the given expression. |
| ~SPC m e~ | Show the context of the goal at point. |
| ~SPC m f~ | Go to the next goal, if any and activate goal-navigation micro-state. |
| ~SPC m h~ | Compute the type of a hypothetical helper function. |
| ~SPC m l~ | Load current buffer. |
| ~SPC m n~ | Computes the normal form of the given expression, using the scope of the current goal or, if point is not in a goal, the top-level scope. |
| ~SPC m o~ | Shows all the top-level names in the given module. |
| ~SPC m r~ | Refine the goal at point. |
| ~SPC m s~ | Solves all goals that are already instantiated internally. |
| ~SPC m t~ | Show the type of the goal at point. |
| ~SPC m x c~ | Compile current module. |
| ~SPC m x d~ | Removes buffer annotations (overlays and text properties). |
| ~SPC m x h~ | Toggle display of implicit arguments. |
| ~SPC m x q~ | Quit and clean up after agda2. |
| ~SPC m x r~ | Kill and restart the *agda2* buffer and load =agda2-toplevel-module=. |
| ~SPC m w~ | Explains why a given name is in scope. |
