Could %:split could emit a let-expression when there's a unique case?

[tsani]

I think the answer is yes. It should suffice to analyze the case-expression generated by the splitting to see if it is a unique case, and then to convert from a case-expression to a let-expression. For a better solution, perhaps, we could adjust the splitting algorithm at a slightly lower level to simply generate a let-expression in the first place if the list of patterns is a singleton.

[tsani]

Following discussion with @pientka yesterday, the answer is basically "yes", but we should be midful of #16 (first-class lets). Presently, let-bindings are simply desugared to case-expressions, which can sometimes make the totality checker go haywire, since it can no longer tell that a new name given to some expression that it knew to be structurally smaller is in fact still structurally smaller.

By introducing a new let expression in the internal syntax, we can establish that a name is in fact a true synonym for another expression, and make the totality checker aware of this.

This change can be made incrementally: at first we can add the new internal syntax without yet changing the external syntax. Then we can adjust the translation from external to internal syntax to convert non-pattern matching lets into first-class lets.

By separating these two changes, we can implement an interactive mode command %:inductivehypotheses that gives a list of available inductive hypotheses at a given hole.

This command can then be used to implement a new beluga-mode command beluga-invoke-ih that lets the user select an inductive hypothesis and generates a let-expression for it at the current hole.

[tsani]

Given that this issue relates to the Emacs interactive mode that has been largely replaced by Harpoon, this issue is low priority.