Adds theorem and proof construct [new base]

[nskh]

Replaces #1263, #1308.

In-progress PR to add a theorem keyword in the style of let-equals-in to Hazel.

Based on editor-output this time.

TODO:

• change sorting to theorem pat = exp in exp, which matches let expressions exactly
• have theorem behave exactly like a let expression everywhere else in the codebase
• at the type level, rename existing forall to type
• add new forall pat -> ty construct to types
• add {e1 = e2} form to types
• syntax highlighting for the pattern in the forall type
• change "=" to "proof" in syntax
• explainthis documentation for new constructs
• cursor inspector behavior for new constructs
• Theorem explainthis should be different from let
• elaboration (same as let expression)
• Static analysis within new constructs?
• Fix stack overflow

[thomasporter522]

Should foralls be annotated? forall pat : ty -> ty ?

[cyrus-]

No, pat includes compositional support for (multiple) type annotations already.

[thomasporter522]

I am unable to make sense of the error messages for the automatic build action, sorry

[cyrus-]

@thomasporter522 those messages are from the automatic code formatter needing to fix the formatting. you should make sure the autoformatting is run before commiting. may also be a make deps issue, make sure you have the same formatter version as the one the build script is using.

[thomasporter522]

Local issue: If you type:

let y : forall x -> = in

Then, after the arrow, type

{x}

Then press the left arrow key, the program will crash due to something related to the head of an empty list or something about "nonconvex segment."

[cyrus-]

No idea what is going on there -- maybe @disconcision or @dm0n3y have an idea?

[disconcision]

@thomasporter522 to clarify, what you've written is bad syntax yes as the {}s require a =?

three-delimiter forms have never been 100% functional in hazel3. all of the existing ones break with a nonconvex segment error if you try to delete the middle delimiter while the others are not in the backpack (e.g. try to delete the = for a let). this is likely the same or a closely related issue; it might be somewhat different since technically we've never tried to implement a convex tile with three delimiters.

this is related to core segment logic which i don't really understand. unless @dm0n3y wants to attempt a fix, you might be able to work around this by making [{, }] and [=] separate forms which are parsed together in MakeTerm, similar to how tuples and list literals are. you could also make their decorations conjoined using similar logic.

[thomasporter522]

@disconcision The answer to your clarification is "yes". Thanks for the explanation and possible workaround. Do you think the upcoming syntax model fix the issue?

[disconcision]

yes, the upcoming syntax model fully accounts for this case, so whether the workaround is worth it depends on timelines

[cyrus-]

closing in favor of #1376