Sebastian Graf 220a242f65 feat: add @[mvcgen_invariant_type] attribute for extensible invariant classification (#12874) ...

This PR adds an `@[mvcgen_invariant_type]` tag attribute so that users
can mark
custom types as invariant types for the `mvcgen` tactic. Goals whose
type is an
application of a tagged type are classified as invariants rather than
verification
conditions. The hard-coded check for `Std.Do.Invariant` is kept as a
fallback
until a stage0 update allows applying the attribute directly.

A follow-up PR (after a stage0 update) will apply
`@[mvcgen_invariant_type]` to
`Std.Do.Invariant` and remove the hard-coded fallback.

---------

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

2026-03-11 08:04:22 +00:00

..

src

feat: add @[mvcgen_invariant_type] attribute for extensible invariant classification (#12874)

2026-03-11 08:04:22 +00:00

stdlib

chore: update stage0

2026-03-10 13:16:48 +00:00