Karl Palmskog (Oct 05 2022 at 20:01): Karl Palmskog (Oct 05 2022 at 20:01):Interesting paper by Danvy on using fold-unfold lemmas in Coq, primarily based on his experience teaching functional programming + proofs. Would have been nicer with the Alectryon-hydras toolchain though, no source...
Last updated: Jun 11 2023 at 01:30 UTC