verus-lang / verus-analyzer

A Verus compiler front-end for IDEs (derived from rust-analyzer)
Apache License 2.0
8 stars 4 forks source link

Merge Proof action to main #22

Closed chanheec closed 5 months ago

chanheec commented 5 months ago

This PR adds proof-action, an experimental feature to assist developers in debugging their failing proofs.

It is not enabled by default but can be enabled by passing the --proof-action flag when a user builds this verus-analyzer.

It is conditionally compiled depending on the proof-action feature.