search

flyvy-verifier / flyvy

An experimental framework for temporal verification based on first-order linear-time temporal logic. Our goal is to express transition systems in first-order logic and verify temporal correctness properties, including safety and liveness.
BSD 2-Clause "Simplified" License
14 stars 1 forks source link

Make Spanned hold an Option<Span> #137

Closed Alex-Fischman closed 1 year ago

Alex-Fischman commented 1 year ago

This PR makes Spanned<T> hold an Option<Span> instead of a Span. It also removes MaybeSpannedTerm from transitions.rs, as it is no longer necessary.