More annotation syntax

[coord-e]

extracted from #18

• <t>, <t1, t2>
• Sort parameters, currently parses as Tn as ad-hoc way
• Boolean terms (true, false)
• Pointer sorts &mut S, &S

[Copilot]

Pull request overview

This PR adds new annotation syntax for Thrust, extracted from PR #18, enabling more expressive type refinements and specifications.

• Adds support for boolean literals (true, false) in both formula and term contexts
• Introduces box and mutable reference term syntax using angle brackets: <t> for box terms and <t1, t2> for mutable reference terms
• Adds pointer sort syntax using ampersands: &S for box sorts and &mut S for mutable reference sorts
• Implements ad-hoc parsing for type parameters using the pattern Tn (e.g., T0, T1)

Reviewed changes

Copilot reviewed 5 out of 5 changed files in this pull request and generated 1 comment.

Show a summary per file

File	Description
tests/ui/pass/annot_mut_term.rs	Test case verifying mutable reference term syntax <*x, y> in ensures clause
tests/ui/pass/annot_box_term.rs	Test case verifying box term syntax <x> in function signatures and requires clauses
tests/ui/fail/annot_mut_term.rs	Negative test ensuring mutable reference term verification correctly fails
tests/ui/fail/annot_box_term.rs	Negative test ensuring box term verification correctly fails
src/annot.rs	Core implementation adding FormulaOrTerm::Literal variant, parsing logic for <> term syntax, & sort syntax, and Tn sort parameters

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.