aeneas/backends/IsabelleHOL, branch isabelle aeneas rust verifier with a hacky Isabelle backend isabelle: more correct u32 type 2024-07-04T14:23:25+00:00 stuebinm 2024-07-04T14:23:25+00:00 bd4c7558b96b0616023b4e4600a73a82ab2a9a3d (I'd have to figure out how to do the code equation stuff to make this type actually usable the way nat is, but it should behave correctly in proofs) 
(I'd have to figure out how to do the code equation stuff to make this
type actually usable the way nat is, but it should behave correctly in
proofs)
had some fun writing an IsabelleHOL backend 2024-06-29T20:11:04+00:00 stuebinm 2024-06-29T19:31:22+00:00 59214186b817329342d9d72e23adf12f7a3b1348 (do not actually use this, most things are broken, and the primitives lib barely exists and is simply incorrect. But it is enough to create syntax-correct Isabelle code for relatively simply rust code, as long as it does not contain any uses of traits) 
(do not actually use this, most things are broken, and the primitives
lib barely exists and is simply incorrect. But it is enough to create
syntax-correct Isabelle code for relatively simply rust code, as long
as it does not contain any uses of traits)