aeneas/compiler, branch isabelle

had some fun writing an IsabelleHOL backend

2024-06-29T20:11:04Z

(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)

Remove redundant `llbc_name` field

2024-06-28T07:46:11Z

It's redundant with `item_meta.name`

Update charon

2024-06-25T11:57:52Z

Update charon

2024-06-24T11:53:31Z

Update charon

2024-06-21T14:14:58Z

`predicates` got merged into `generic_params`

2024-06-21T07:34:38Z

Support for renaming using the rename attribute in charon (#239)

2024-06-18T20:47:35Z

* support for renaming using the rename attribute in charon * support for global decl * add support for renaming field * applied suggested changes and began adding support for variant * finished support for renaming variant * applied suggested changes * add tests * fixed variant and field renaming * update charon-pin * update flake.lock * Update the charon pin * Fix an issue with renaming trait method implementations * Fix an issue with the renaming of trait implementations * Fix an issue when renaming enumerations * Update the Charon pin * Fix the F* tests * Fix an issue with the spans for the loops * Fix the tests * Update a comment * Use fuel in the coq tests * Generate the template decreases clauses by default --------- Co-authored-by: Escherichia Co-authored-by: Son Ho

Tiny dedup

2024-06-18T10:11:23Z

Deactivate some linter options for the generated Lean files

2024-06-17T05:25:00Z

Automatically add a @[reducible] attribute to some generated functions

2024-06-17T05:14:52Z