Re:Lean proved this program correct; then I found a bug
by DonaldPShimoda on Tuesday April 14, 2026 @12:18PM
(#47767621)
> finite programs that run on an infinite stream of events
This requires coinduction, right? (That's my understanding of the formal representation of infinite streams.) If so, that does limit your options, since most of the proof assistants don't handle coinductive data, as I understand it.
This requires coinduction, right? (That's my understanding of the formal representation of infinite streams.) If so, that does limit your options, since most of the proof assistants don't handle coinductive data, as I understand it.