Hacker News Reader

Interesting! Looks most similar to Creusot. The syntax is definitely nicer but wrapping your entire code in a macro surely is going to upset rust-analyzer?

View on HN

A fork of rust-analyzer, called verus-analyzer, provides support for Verus syntax and actions (including new proof-specific actions) https://github.com/verus-lang/verus-analyzer/

I’m not sure how rust-analyser works, but presumably you’d make the macro a no-op and just return the original tokens in debug builds

Reply on news.ycombinator.com