Issues · AeneasVerif/aeneas · GitHub

Labels Milestones New issue

Internal error translating a function that returns a closure which borrows its environment (`-> impl Fn + 'a`)

#1119

· strub opened

on Jun 11, 2026

Rocq Axiom `mk_array` is unsound

#1116

· niooss-ledger opened

on Jun 10, 2026

Add support for GATs

#1112

· Nadrieril opened

on Jun 10, 2026

Bug: `#decompose` doesn't handle pure tuple decompositions

#1110

· sonmarcho opened

on Jun 10, 2026

feat: Update #decompose to allow using expressions

#1109

· sonmarcho opened

on Jun 9, 2026

Remove the custom `Range` definitions

#1107

· sonmarcho opened

on Jun 9, 2026

Bug: `name` is a keyword in the Lean backend

#1105

· sonmarcho opened

on Jun 8, 2026

Uncaught Not_found in trait_impl_is_builtin (Translate.ml:1017)

#1102

· dhsorens opened

on Jun 4, 2026

Fail to translate function with double reference and try (`?`)

#1099

· niooss-ledger opened

on Jun 3, 2026

Name clash between variable and module

#1098

· maximebuyse opened

on Jun 2, 2026

Per-target instance bodies of `target_dispatch` items dropped under multi-target extraction

#1077

· fournet opened

on May 28, 2026

`Iterator::zip` test check fails with `RErased`

#1053

· waamm opened

on May 22, 2026