aeneas/tests/coq/betree/_CoqProject, branch isabelle aeneas rust verifier with a hacky Isabelle backend https://stuebinm.eu/git/aeneas/atom/tests/coq/betree/_CoqProject?h=isabelle 2024-05-28T09:36:31Z tests: Rename betree_main -> betree 2024-05-28T09:36:31Z Nadrieril 2024-05-27T11:28:28Z urn:sha1:f77e3f9cbe2ea7abeb4be815bdbf33d0c98076c2 Regenerate the tests 2024-03-19T04:29:29Z Son Ho 2024-03-19T04:29:29Z urn:sha1:f3e16bb43a8ff27a5184d9fa452277cc6a59410f Generate a dedicated file for the external types 2023-11-27T09:29:25Z Son Ho 2023-11-27T09:29:25Z urn:sha1:bef2bd34fcb0817f1b7d16b95122bcc3c6f05c72 Update the generation of files for external definitions and regenerate the tests 2023-11-27T08:37:31Z Son Ho 2023-11-27T08:37:31Z urn:sha1:959d6fce38c8d8ca6eaed3ad6f458b87f91a9abc Improve the generated comments 2023-07-06T10:20:28Z Son Ho 2023-07-06T10:20:28Z urn:sha1:7c95800cefc87fad894f8bf855cfc047e713b3a7 Make sure let-bindings in Lean end with line breaks and improve formatting 2023-06-04T19:44:33Z Son Ho 2023-02-05T21:03:41Z urn:sha1:c6913b8bf90689d8961c47f59896443e7fae164d Automatically generate the Makefile and _CoqProject files in the tests subdirectories 2022-11-16T14:45:32Z Son Ho 2022-11-16T13:40:34Z urn:sha1:a20819f170acc6aad7b5aca2fbe53c7b3ab7e2b8 Generate record field projectors for Coq 2022-11-16T14:45:32Z Son Ho 2022-11-15T15:32:35Z urn:sha1:8bf0452f91c44ff390556db77bf42697c0443b67 Extract the Polonius examples in Coq 2022-11-14T13:21:04Z Son Ho 2022-11-14T13:14:38Z urn:sha1:6f714017d71a512042b22d7d0e987f75b47a088f